environ
vocabularies HIDDEN, NUMBERS, XXREAL_1, REAL_1, PRE_TOPC, TOPMETR, XXREAL_0, STRUCT_0, SUBSET_1, RCOMP_1, PCOMPS_1, METRIC_1, CARD_1, TARSKI, ARYTM_1, ARYTM_3, FUNCT_1, COMPLEX1, SETFAM_1, XBOOLE_0, VALUED_1, BORSUK_1, RELAT_1, ORDINAL2, TMAP_1, TOPS_2, RELAT_2, XXREAL_2, SEQ_4, FUNCT_3, TREAL_1, FUNCT_2, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XXREAL_2, XREAL_0, COMPLEX1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, REAL_1, SEQ_4, RCOMP_1, PRE_TOPC, TOPS_2, CONNSP_1, METRIC_1, DOMAIN_1, STRUCT_0, PCOMPS_1, TOPMETR, TSEP_1, TMAP_1, BORSUK_1;
definitions TARSKI, FUNCT_2, XXREAL_2;
theorems TARSKI, SUBSET_1, FUNCT_1, FUNCT_2, ABSVALUE, RCOMP_1, SEQ_2, SEQ_4, METRIC_1, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_1, PCOMPS_1, BORSUK_1, TOPMETR, HEINE, TSEP_1, TMAP_1, RELAT_1, TBSP_1, RELSET_1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0, XXREAL_1;
schemes FUNCT_2;
registrations XBOOLE_0, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, BORSUK_1, TOPMETR, CONNSP_1, ORDINAL1;
constructors HIDDEN, REAL_1, SQUARE_1, COMPLEX1, SEQ_4, RCOMP_1, CONNSP_1, TOPS_2, TMAP_1, TOPMETR, XXREAL_2, BINOP_2, RVSUM_1, PCOMPS_1, BINOP_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities SUBSET_1, STRUCT_0;
expansions TARSKI, FUNCT_2, XXREAL_2;
Lm1:
for a, b being Real
for x being set st x in [.a,b.] holds
x is Element of REAL
;
Lm2:
for a, b being Real
for x being Point of (Closed-Interval-TSpace (a,b)) st a <= b holds
x is Element of REAL
definition
let a,
b be
Real;
assume A1:
a <= b
;
let t1,
t2 be
Point of
(Closed-Interval-TSpace (a,b));
existence
ex b1 being Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) st
for s being Point of (Closed-Interval-TSpace (0,1)) holds b1 . s = ((1 - s) * t1) + (s * t2)
uniqueness
for b1, b2 being Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) st ( for s being Point of (Closed-Interval-TSpace (0,1)) holds b1 . s = ((1 - s) * t1) + (s * t2) ) & ( for s being Point of (Closed-Interval-TSpace (0,1)) holds b2 . s = ((1 - s) * t1) + (s * t2) ) holds
b1 = b2
end;
definition
let a,
b be
Real;
assume A1:
a < b
;
let t1,
t2 be
Point of
(Closed-Interval-TSpace (0,1));
existence
ex b1 being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) st
for s being Point of (Closed-Interval-TSpace (a,b)) holds b1 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a)
uniqueness
for b1, b2 being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) st ( for s being Point of (Closed-Interval-TSpace (a,b)) holds b1 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ) & ( for s being Point of (Closed-Interval-TSpace (a,b)) holds b2 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ) holds
b1 = b2
end;
::
deftheorem Def4 defines
P[01] TREAL_1:def 4 :
for a, b being Real st a < b holds
for t1, t2 being Point of (Closed-Interval-TSpace (0,1))
for b5 being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) holds
( b5 = P[01] (a,b,t1,t2) iff for s being Point of (Closed-Interval-TSpace (a,b)) holds b5 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) );
theorem
for
a,
b being
Real st
a < b holds
for
t1,
t2 being
Point of
(Closed-Interval-TSpace (0,1)) holds
(
(P[01] (a,b,t1,t2)) . ((#) (a,b)) = t1 &
(P[01] (a,b,t1,t2)) . ((a,b) (#)) = t2 )
theorem Th15:
for
a,
b being
Real st
a < b holds
(
id (Closed-Interval-TSpace (a,b)) = (L[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#)))) &
id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((#) (0,1)),((0,1) (#)))) * (L[01] (((#) (a,b)),((a,b) (#)))) )
theorem Th16:
for
a,
b being
Real st
a < b holds
(
id (Closed-Interval-TSpace (a,b)) = (L[01] (((a,b) (#)),((#) (a,b)))) * (P[01] (a,b,((0,1) (#)),((#) (0,1)))) &
id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b)))) )
theorem Th17:
for
a,
b being
Real st
a < b holds
(
L[01] (
((#) (a,b)),
((a,b) (#))) is
being_homeomorphism &
(L[01] (((#) (a,b)),((a,b) (#)))) " = P[01] (
a,
b,
((#) (0,1)),
((0,1) (#))) &
P[01] (
a,
b,
((#) (0,1)),
((0,1) (#))) is
being_homeomorphism &
(P[01] (a,b,((#) (0,1)),((0,1) (#)))) " = L[01] (
((#) (a,b)),
((a,b) (#))) )
theorem
for
a,
b being
Real st
a < b holds
(
L[01] (
((a,b) (#)),
((#) (a,b))) is
being_homeomorphism &
(L[01] (((a,b) (#)),((#) (a,b)))) " = P[01] (
a,
b,
((0,1) (#)),
((#) (0,1))) &
P[01] (
a,
b,
((0,1) (#)),
((#) (0,1))) is
being_homeomorphism &
(P[01] (a,b,((0,1) (#)),((#) (0,1)))) " = L[01] (
((a,b) (#)),
((#) (a,b))) )