environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI, BORSUK_2, XBOOLE_0, XXREAL_2, PRE_TOPC, PSCOMP_1;
theorems BORSUK_1, COMPTS_1, CONNSP_2, EUCLID, FCONT_1, FCONT_2, FUNCT_1, FUNCT_2, GOBOARD7, GOBOARD9, METRIC_1, PARTFUN2, PCOMPS_1, PRE_TOPC, RCOMP_1, RELAT_1, RFUNCT_2, SEQ_4, TARSKI, TBSP_1, TMAP_1, TOPMETR, TOPREAL1, TOPS_2, TOPS_1, WEIERSTR, TOPREAL3, RELSET_1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, XXREAL_2, XXREAL_1, MEMBERED, MEASURE6, HEINE, RLVECT_1;
schemes CLASSES1;
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;
constructors HIDDEN, 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;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities STRUCT_0, RLTOPSP1, SUBSET_1, RLVECT_1;
expansions TARSKI, BORSUK_2, XBOOLE_0, XXREAL_2, PRE_TOPC;
Lm1:
for n being Nat holds
( the carrier of (Euclid n) = REAL n & the carrier of (TOP-REAL n) = REAL n )
theorem Th2:
for
n being
Nat for
p1,
p2 being
Point of
(TOP-REAL n) for
r1,
r2 being
Real holds
( not
((1 - r1) * p1) + (r1 * p2) = ((1 - r2) * p1) + (r2 * p2) or
r1 = r2 or
p1 = p2 )
Lm2:
for n being Nat holds TOP-REAL n is pathwise_connected
Lm3:
for X being Subset of REAL st X is open holds
X in Family_open_set RealSpace
Lm4:
for X being Subset of REAL st X in Family_open_set RealSpace holds
X is open
Lm5:
for f being one-to-one continuous Function of R^1,R^1
for g being PartFunc of REAL,REAL holds
( not f = g or g | [.0,1.] is increasing or g | [.0,1.] is decreasing )
Lm6:
for a, b, c being Real st a <= b holds
( c in the carrier of (Closed-Interval-TSpace (a,b)) iff ( a <= c & c <= b ) )
Lm7:
for a, b, c, d being Real
for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d))
for x being Point of (Closed-Interval-TSpace (a,b))
for g being PartFunc of REAL,REAL
for x1 being Real st a < b & c < d & f is_continuous_at x & x <> a & x <> b & f . a = c & f . b = d & f is one-to-one & f = g & x = x1 holds
g is_continuous_in x1
theorem Th13:
for
a,
b,
c,
d,
x1 being
Real for
f being
Function of
(Closed-Interval-TSpace (a,b)),
(Closed-Interval-TSpace (c,d)) for
x being
Point of
(Closed-Interval-TSpace (a,b)) for
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 Th15:
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 &
f is
one-to-one &
f . a = c &
f . b = d holds
for
x,
y being
Point of
(Closed-Interval-TSpace (a,b)) for
p,
q,
fx,
fy being
Real st
x = p &
y = q &
p < q &
fx = f . x &
fy = f . y holds
fx < fy
theorem
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.]
Lm8:
R^1 = TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #)
by PCOMPS_1:def 5, TOPMETR:def 6;