:: Some Properties of Real Maps
:: by Adam Grabowski and Yatsuka Nakamura
::
:: Received September 10, 1997
:: Copyright (c) 1997-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, PRE_TOPC, EUCLID, TOPREAL1, RCOMP_1, FUNCT_1,
BORSUK_1, RELAT_1, TOPS_2, CARD_1, XBOOLE_0, ORDINAL2, STRUCT_0,
METRIC_1, ARYTM_1, ARYTM_3, SUPINF_2, RLTOPSP1, REAL_1, XXREAL_1, TARSKI,
XXREAL_0, PCOMPS_1, CONNSP_2, TOPMETR, TOPS_1, COMPLEX1, BORSUK_2,
GRAPH_1, PARTFUN1, TMAP_1, FCONT_1, VALUED_0, SEQ_4, XXREAL_2, FUNCT_2,
PSCOMP_1, FINSET_1, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, COMPLEX1, XXREAL_2, REAL_1, RELAT_1, FUNCT_1, RELSET_1,
FINSET_1, PARTFUN1, FUNCT_2, FCONT_1, RFUNCT_2, SEQ_4, MEASURE6, TOPMETR,
BINOP_1, TOPS_1, METRIC_1, CONNSP_2, STRUCT_0, TOPREAL1, PRE_TOPC,
TOPS_2, COMPTS_1, RLVECT_1, RLTOPSP1, EUCLID, TMAP_1, PSCOMP_1, PCOMPS_1,
WEIERSTR, BORSUK_2, RCOMP_1;
constructors REAL_1, SQUARE_1, COMPLEX1, SEQ_4, RCOMP_1, FCONT_1, TOPS_1,
TOPS_2, COMPTS_1, TMAP_1, TOPREAL1, WEIERSTR, BORSUK_2, RVSUM_1, CONVEX1,
BINOP_2, PSCOMP_1, MEASURE6, BINOP_1;
registrations XBOOLE_0, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED,
RCOMP_1, STRUCT_0, PRE_TOPC, METRIC_1, BORSUK_1, EUCLID, TOPMETR,
TOPREAL1, PSCOMP_1, BORSUK_2, VALUED_0, COMPTS_1, XXREAL_2, RLTOPSP1,
FCONT_1, FUNCT_2, FUNCT_1, TOPS_1, SUBSET_1, FINSET_1, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries
theorem :: JORDAN5A:1
for n being Nat, p, q being Point of TOP-REAL n, P
being Subset of TOP-REAL n st P is_an_arc_of p, q holds P is compact;
theorem :: JORDAN5A:2
for n being Nat, p1, p2 being Point of TOP-REAL n, r1,
r2 being Real st (1-r1)*p1+r1*p2 = (1-r2)*p1+r2*p2 holds r1 = r2 or p1 =
p2;
theorem :: JORDAN5A:3
for n being Nat for p1,p2 being Point of TOP-REAL n st
p1 <> p2 ex f being Function of I[01], (TOP-REAL n) | LSeg(p1,p2) st (for x
being Real st x in [.0,1.] holds f.x = (1-x)*p1 + x*p2) & f is
being_homeomorphism & f.0 = p1 & f.1 = p2;
registration
let n be Nat;
cluster TOP-REAL n -> pathwise_connected;
end;
registration
let n be Nat;
cluster compact non empty strict for SubSpace of TOP-REAL n;
end;
theorem :: JORDAN5A:4
for a, b being Point of TOP-REAL 2, f being Path of a, b, P being non
empty compact SubSpace of TOP-REAL 2, g being Function of I[01], P st f is
one-to-one & g = f & [#]P = rng f holds g is being_homeomorphism;
begin
:: Equivalence of analytical and topological definitions of continuity
theorem :: JORDAN5A:5
for X being Subset of REAL holds X in Family_open_set RealSpace iff X
is open;
theorem :: JORDAN5A:6
for f being Function of R^1, R^1, x being Point of R^1 for g
being PartFunc of REAL, REAL, x1 being Real
st f is_continuous_at x & f = g & x = x1 holds g is_continuous_in x1;
theorem :: JORDAN5A:7
for f being continuous Function of R^1, R^1, g being PartFunc of
REAL, REAL st f = g holds g is continuous;
theorem :: JORDAN5A:8
for f being continuous one-to-one Function of R^1, R^1 holds (for x, y
being Point of I[01], p, q, fx, fy being Real
st x = p & y = q & p < q & fx = f
.x & fy = f.y holds fx < fy) or
for x, y being Point of I[01], p, q, fx, fy being Real
st x = p & y = q & p < q & fx = f.x & fy = f.y holds fx > fy;
theorem :: JORDAN5A:9
for r, gg, a, b being Real, x being Element of
Closed-Interval-MSpace (a, b) st a <= b & x = r & ].r-gg, r+gg.[ c= [.a,b.]
holds ].r-gg, r+gg.[ = Ball (x, gg);
theorem :: JORDAN5A:10
for a, b being Real, X being Subset of REAL st a < b & not a in
X & not b in X holds X in Family_open_set Closed-Interval-MSpace(a,b) implies X
is open;
theorem :: JORDAN5A:11
for X being open Subset of REAL, a, b being Real st X c= [.a,b.]
holds not a in X & not b in X;
theorem :: JORDAN5A:12
for a, b being Real, X being Subset of REAL, V being Subset of
Closed-Interval-MSpace(a,b) st V = X holds X is open implies V in
Family_open_set Closed-Interval-MSpace(a,b);
theorem :: JORDAN5A:13
for a, b, c, d, x1 being Real, f being Function of
Closed-Interval-TSpace(a,b), Closed-Interval-TSpace(c,d), x being Point of
Closed-Interval-TSpace(a,b), g being PartFunc of REAL, REAL st a < b & c < d &
f is_continuous_at x & f.a = c & f.b = d & f is one-to-one & f = g & x = x1
holds g| [.a,b.] is_continuous_in x1;
theorem :: JORDAN5A:14
for a, b, c, d being Real, f being Function of
Closed-Interval-TSpace(a,b), Closed-Interval-TSpace(c,d), g being PartFunc of
REAL, REAL st f is continuous one-to-one & a < b & c < d & f = g & f.a = c & f.
b = d holds g| [.a,b.] is continuous;
begin
:: On the monotonicity of continuous maps
theorem :: JORDAN5A:15
for a, b, c, d being Real for f being Function of
Closed-Interval-TSpace(a,b), Closed-Interval-TSpace(c,d) st a < b & c < d & f
is continuous one-to-one & f.a = c & f.b = d holds for x, y be Point of
Closed-Interval-TSpace(a,b),
p, q, fx, fy being Real st x = p & y = q & p < q &
fx = f.x & fy = f.y holds fx < fy;
theorem :: JORDAN5A:16
for f being continuous one-to-one Function of I[01], I[01] st f.0 = 0
& f.1 = 1 holds for x, y being Point of I[01],
p, q, fx, fy being Real st x = p
& y = q & p < q & fx = f.x & fy = f.y holds fx < fy;
theorem :: JORDAN5A:17
for a, b, c, d being Real, f being Function of Closed-Interval-TSpace(
a,b), Closed-Interval-TSpace(c,d), P being non empty Subset of
Closed-Interval-TSpace(a,b), PP, QQ being Subset of R^1 st a < b & c < d & PP =
P & f is continuous one-to-one & PP is compact & f.a = c & f.b = d & f.:P = QQ
holds f.(lower_bound [#]PP) = lower_bound [#]QQ;
theorem :: JORDAN5A:18
for a, b, c, d being Real, f being Function of Closed-Interval-TSpace(
a,b), Closed-Interval-TSpace(c,d), P, Q being non empty Subset of
Closed-Interval-TSpace(a,b), PP, QQ being Subset of R^1 st a < b & c < d & PP =
P & QQ = Q & f is continuous one-to-one & PP is compact & f.a = c & f.b = d & f
.:P = Q holds f.(upper_bound [#]PP) = upper_bound [#]QQ;
theorem :: JORDAN5A:19
for a, b being Real st a <= b holds lower_bound [.a,b.] = a &
upper_bound [.a,b.] = b;
theorem :: JORDAN5A:20
for a, b, c, d, e, f, g, h being Real
for F being Function of
Closed-Interval-TSpace (a,b), Closed-Interval-TSpace (c,d) st a < b & c < d & e
< f & a <= e & f <= b & F is being_homeomorphism & F.a = c & F.b = d & g = F.e
& h = F.f holds F.:[.e, f.] = [.g, h.];
theorem :: JORDAN5A:21
for P, Q being Subset of TOP-REAL 2, p1, p2 being Point of TOP-REAL 2
st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds ex EX being Point
of TOP-REAL 2 st ( EX in P /\ Q &
ex g being Function of I[01], (TOP-REAL 2)|P, s2 being Real
st g is being_homeomorphism & g.0 = p1 & g.1 = p2 & g.s2 = EX & 0
<= s2 & s2 <= 1 &
for t being Real st 0 <= t & t < s2 holds not g.t in Q );
theorem :: JORDAN5A:22
for P, Q being Subset of TOP-REAL 2, p1, p2 being Point of TOP-REAL 2
st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds ex EX be Point of
TOP-REAL 2 st ( EX in P /\ Q &
ex g being Function of I[01], (TOP-REAL 2)|P, s2 being Real
st g is being_homeomorphism & g.0 = p1 & g.1 = p2 & g.s2 = EX & 0 <=
s2 & s2 <= 1 &
for t being Real st 1 >= t & t > s2 holds not g.t in Q );
:: from TOPREAL6, 2011.07.29, A.T.
registration
cluster non empty finite real-bounded for Subset of REAL;
end;
theorem :: JORDAN5A:23
for A being Subset of REAL, B being Subset of R^1 st A = B holds
A is closed iff B is closed;
theorem :: JORDAN5A:24
for A being Subset of REAL, B being Subset of R^1 st A = B holds Cl A = Cl B;
registration
let a, b be Real;
cluster [.a,b.] -> compact for Subset of REAL;
end;
theorem :: JORDAN5A:25
for A being Subset of REAL, B being Subset of R^1 st A = B holds
A is compact iff B is compact;
registration
cluster finite -> compact for Subset of REAL;
end;
theorem :: JORDAN5A:26
for a, b being Real holds a <> b iff Cl ].a,b.[ = [.a,b.];
theorem :: JORDAN5A:27
for T being TopStruct, f being RealMap of T, g being Function of
T, R^1 st f = g holds f is continuous iff g is continuous;