:: TOPREAL1 semantic presentation
begin
scheme :: TOPREAL1:sch 1
FraenkelAlt{ F1() -> non empty set , P1[ set ], P2[ set ] } :
{ v where v is Element of F1() : ( P1[v] or P2[v] ) } = { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] }
proof
set X = { v where v is Element of F1() : ( P1[v] or P2[v] ) } ;
set Y = { v1 where v1 is Element of F1() : P1[v1] } ;
set Z = { v2 where v2 is Element of F1() : P2[v2] } ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in__{__v_where_v_is_Element_of_F1()_:_(_P1[v]_or_P2[v]_)__}__implies_x_in__{__v1_where_v1_is_Element_of_F1()_:_P1[v1]__}__\/__{__v2_where_v2_is_Element_of_F1()_:_P2[v2]__}__)_&_(_x_in__{__v1_where_v1_is_Element_of_F1()_:_P1[v1]__}__\/__{__v2_where_v2_is_Element_of_F1()_:_P2[v2]__}__implies_x_in__{__v_where_v_is_Element_of_F1()_:_(_P1[v]_or_P2[v]_)__}__)_)
let x be set ; ::_thesis: ( ( x in { v where v is Element of F1() : ( P1[v] or P2[v] ) } implies x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } ) & ( x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } implies b1 in { b2 where v is Element of F1() : ( P1[b2] or P2[b2] ) } ) )
thus ( x in { v where v is Element of F1() : ( P1[v] or P2[v] ) } implies x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } ) ::_thesis: ( x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } implies b1 in { b2 where v is Element of F1() : ( P1[b2] or P2[b2] ) } )
proof
assume x in { v where v is Element of F1() : ( P1[v] or P2[v] ) } ; ::_thesis: x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] }
then consider v being Element of F1() such that
A1: x = v and
A2: ( P1[v] or P2[v] ) ;
percases ( P1[v] or P2[v] ) by A2;
suppose P1[v] ; ::_thesis: x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] }
then x in { v1 where v1 is Element of F1() : P1[v1] } by A1;
hence x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose P2[v] ; ::_thesis: x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] }
then x in { v2 where v2 is Element of F1() : P2[v2] } by A1;
hence x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
assume A3: x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } ; ::_thesis: b1 in { b2 where v is Element of F1() : ( P1[b2] or P2[b2] ) }
percases ( x in { v1 where v1 is Element of F1() : P1[v1] } or x in { v2 where v2 is Element of F1() : P2[v2] } ) by A3, XBOOLE_0:def_3;
suppose x in { v1 where v1 is Element of F1() : P1[v1] } ; ::_thesis: b1 in { b2 where v is Element of F1() : ( P1[b2] or P2[b2] ) }
then ex v being Element of F1() st
( x = v & P1[v] ) ;
hence x in { v where v is Element of F1() : ( P1[v] or P2[v] ) } ; ::_thesis: verum
end;
suppose x in { v2 where v2 is Element of F1() : P2[v2] } ; ::_thesis: b1 in { b2 where v is Element of F1() : ( P1[b2] or P2[b2] ) }
then ex v being Element of F1() st
( x = v & P2[v] ) ;
hence x in { v where v is Element of F1() : ( P1[v] or P2[v] ) } ; ::_thesis: verum
end;
end;
end;
hence { v where v is Element of F1() : ( P1[v] or P2[v] ) } = { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } by TARSKI:1; ::_thesis: verum
end;
definition
let T be TopSpace;
let p1, p2 be Point of T;
let P be Subset of T;
predP is_an_arc_of p1,p2 means :Def1: :: TOPREAL1:def 1
ex f being Function of I[01],(T | P) st
( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 );
end;
:: deftheorem Def1 defines is_an_arc_of TOPREAL1:def_1_:_
for T being TopSpace
for p1, p2 being Point of T
for P being Subset of T holds
( P is_an_arc_of p1,p2 iff ex f being Function of I[01],(T | P) st
( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) );
theorem Th1: :: TOPREAL1:1
for T being TopSpace
for P being Subset of T
for p1, p2 being Point of T st P is_an_arc_of p1,p2 holds
( p1 in P & p2 in P )
proof
let T be TopSpace; ::_thesis: for P being Subset of T
for p1, p2 being Point of T st P is_an_arc_of p1,p2 holds
( p1 in P & p2 in P )
let P be Subset of T; ::_thesis: for p1, p2 being Point of T st P is_an_arc_of p1,p2 holds
( p1 in P & p2 in P )
let p1, p2 be Point of T; ::_thesis: ( P is_an_arc_of p1,p2 implies ( p1 in P & p2 in P ) )
assume P is_an_arc_of p1,p2 ; ::_thesis: ( p1 in P & p2 in P )
then consider f being Function of I[01],(T | P) such that
A1: f is being_homeomorphism and
A2: f . 0 = p1 and
A3: f . 1 = p2 by Def1;
A4: dom f = [#] I[01] by A1, TOPS_2:def_5
.= the carrier of I[01] ;
1 in [.0,1.] by XXREAL_1:1;
then A5: p2 in rng f by A3, A4, BORSUK_1:40, FUNCT_1:def_3;
A6: rng f = [#] (T | P) by A1, TOPS_2:def_5;
0 in [.0,1.] by XXREAL_1:1;
then p1 in rng f by A2, A4, BORSUK_1:40, FUNCT_1:def_3;
hence ( p1 in P & p2 in P ) by A5, A6, PRE_TOPC:def_5; ::_thesis: verum
end;
theorem Th2: :: TOPREAL1:2
for T being T_2 TopSpace
for P, Q being Subset of T
for p1, p2, q1 being Point of T st P is_an_arc_of p1,p2 & Q is_an_arc_of p2,q1 & P /\ Q = {p2} holds
P \/ Q is_an_arc_of p1,q1
proof
let T be T_2 TopSpace; ::_thesis: for P, Q being Subset of T
for p1, p2, q1 being Point of T st P is_an_arc_of p1,p2 & Q is_an_arc_of p2,q1 & P /\ Q = {p2} holds
P \/ Q is_an_arc_of p1,q1
let P, Q be Subset of T; ::_thesis: for p1, p2, q1 being Point of T st P is_an_arc_of p1,p2 & Q is_an_arc_of p2,q1 & P /\ Q = {p2} holds
P \/ Q is_an_arc_of p1,q1
let p1, p2, q1 be Point of T; ::_thesis: ( P is_an_arc_of p1,p2 & Q is_an_arc_of p2,q1 & P /\ Q = {p2} implies P \/ Q is_an_arc_of p1,q1 )
assume that
A1: P is_an_arc_of p1,p2 and
A2: Q is_an_arc_of p2,q1 and
A3: P /\ Q = {p2} ; ::_thesis: P \/ Q is_an_arc_of p1,q1
consider f2 being Function of I[01],(T | Q) such that
A4: f2 is being_homeomorphism and
A5: f2 . 0 = p2 and
A6: f2 . 1 = q1 by A2, Def1;
consider f1 being Function of I[01],(T | P) such that
A7: f1 is being_homeomorphism and
A8: f1 . 0 = p1 and
A9: f1 . 1 = p2 by A1, Def1;
consider h being Function of I[01],(T | (P \/ Q)) such that
A10: h is being_homeomorphism and
A11: h . 0 = f1 . 0 and
A12: h . 1 = f2 . 1 by A3, A7, A9, A4, A5, TOPMETR2:3;
take h ; :: according to TOPREAL1:def_1 ::_thesis: ( h is being_homeomorphism & h . 0 = p1 & h . 1 = q1 )
thus ( h is being_homeomorphism & h . 0 = p1 & h . 1 = q1 ) by A8, A6, A10, A11, A12; ::_thesis: verum
end;
definition
func R^2-unit_square -> Subset of (TOP-REAL 2) equals :: TOPREAL1:def 2
((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|)));
coherence
((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|))) is Subset of (TOP-REAL 2) ;
end;
:: deftheorem defines R^2-unit_square TOPREAL1:def_2_:_
R^2-unit_square = ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|)));
Lm1: for n being Nat
for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) holds
LSeg (p1,p) c= LSeg (p1,p2)
proof
let n be Nat; ::_thesis: for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) holds
LSeg (p1,p) c= LSeg (p1,p2)
let p, p1, p2 be Point of (TOP-REAL n); ::_thesis: ( p in LSeg (p1,p2) implies LSeg (p1,p) c= LSeg (p1,p2) )
assume p in LSeg (p1,p2) ; ::_thesis: LSeg (p1,p) c= LSeg (p1,p2)
then consider r being Real such that
A1: p = ((1 - r) * p1) + (r * p2) and
A2: 0 <= r and
A3: r <= 1 ;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in LSeg (p1,p) or q in LSeg (p1,p2) )
assume q in LSeg (p1,p) ; ::_thesis: q in LSeg (p1,p2)
then consider b being Real such that
A4: q = ((1 - b) * p1) + (b * p) and
A5: 0 <= b and
A6: b <= 1 ;
A7: q = ((1 - b) * p1) + ((b * ((1 - r) * p1)) + (b * (r * p2))) by A1, A4, EUCLID:32
.= (((1 - b) * p1) + (b * ((1 - r) * p1))) + (b * (r * p2)) by EUCLID:26
.= (((1 - b) * p1) + ((b * (1 - r)) * p1)) + (b * (r * p2)) by EUCLID:30
.= (((1 - b) + (b * (1 - r))) * p1) + (b * (r * p2)) by EUCLID:33
.= ((1 - (b * r)) * p1) + ((b * r) * p2) by EUCLID:30 ;
b * r <= 1 by A2, A3, A6, XREAL_1:160;
hence q in LSeg (p1,p2) by A2, A5, A7; ::_thesis: verum
end;
theorem :: TOPREAL1:3
for p1, p2, p being Point of (TOP-REAL 2) st p1 `1 <= p2 `1 & p in LSeg (p1,p2) holds
( p1 `1 <= p `1 & p `1 <= p2 `1 )
proof
let p1, p2, p be Point of (TOP-REAL 2); ::_thesis: ( p1 `1 <= p2 `1 & p in LSeg (p1,p2) implies ( p1 `1 <= p `1 & p `1 <= p2 `1 ) )
assume that
A1: p1 `1 <= p2 `1 and
A2: p in LSeg (p1,p2) ; ::_thesis: ( p1 `1 <= p `1 & p `1 <= p2 `1 )
consider lambda being Real such that
A3: p = ((1 - lambda) * p1) + (lambda * p2) and
A4: 0 <= lambda and
A5: lambda <= 1 by A2;
A6: ((1 - lambda) * p1) `1 = |[((1 - lambda) * (p1 `1)),((1 - lambda) * (p1 `2))]| `1 by EUCLID:57
.= (1 - lambda) * (p1 `1) by EUCLID:52 ;
A7: (lambda * p2) `1 = |[(lambda * (p2 `1)),(lambda * (p2 `2))]| `1 by EUCLID:57
.= lambda * (p2 `1) by EUCLID:52 ;
A8: p `1 = |[((((1 - lambda) * p1) `1) + ((lambda * p2) `1)),((((1 - lambda) * p1) `2) + ((lambda * p2) `2))]| `1 by A3, EUCLID:55
.= ((1 - lambda) * (p1 `1)) + (lambda * (p2 `1)) by A6, A7, EUCLID:52 ;
lambda * (p1 `1) <= lambda * (p2 `1) by A1, A4, XREAL_1:64;
then ((1 - lambda) * (p1 `1)) + (lambda * (p1 `1)) <= p `1 by A8, XREAL_1:7;
hence p1 `1 <= p `1 ; ::_thesis: p `1 <= p2 `1
0 <= 1 - lambda by A5, XREAL_1:48;
then (1 - lambda) * (p1 `1) <= (1 - lambda) * (p2 `1) by A1, XREAL_1:64;
then p `1 <= ((1 - lambda) * (p2 `1)) + (lambda * (p2 `1)) by A8, XREAL_1:6;
hence p `1 <= p2 `1 ; ::_thesis: verum
end;
theorem :: TOPREAL1:4
for p1, p2, p being Point of (TOP-REAL 2) st p1 `2 <= p2 `2 & p in LSeg (p1,p2) holds
( p1 `2 <= p `2 & p `2 <= p2 `2 )
proof
let p1, p2, p be Point of (TOP-REAL 2); ::_thesis: ( p1 `2 <= p2 `2 & p in LSeg (p1,p2) implies ( p1 `2 <= p `2 & p `2 <= p2 `2 ) )
assume that
A1: p1 `2 <= p2 `2 and
A2: p in LSeg (p1,p2) ; ::_thesis: ( p1 `2 <= p `2 & p `2 <= p2 `2 )
consider lambda being Real such that
A3: p = ((1 - lambda) * p1) + (lambda * p2) and
A4: 0 <= lambda and
A5: lambda <= 1 by A2;
A6: ((1 - lambda) * p1) `2 = |[((1 - lambda) * (p1 `1)),((1 - lambda) * (p1 `2))]| `2 by EUCLID:57
.= (1 - lambda) * (p1 `2) by EUCLID:52 ;
A7: (lambda * p2) `2 = |[(lambda * (p2 `1)),(lambda * (p2 `2))]| `2 by EUCLID:57
.= lambda * (p2 `2) by EUCLID:52 ;
A8: p `2 = |[((((1 - lambda) * p1) `1) + ((lambda * p2) `1)),((((1 - lambda) * p1) `2) + ((lambda * p2) `2))]| `2 by A3, EUCLID:55
.= ((1 - lambda) * (p1 `2)) + (lambda * (p2 `2)) by A6, A7, EUCLID:52 ;
lambda * (p1 `2) <= lambda * (p2 `2) by A1, A4, XREAL_1:64;
then ((1 - lambda) * (p1 `2)) + (lambda * (p1 `2)) <= p `2 by A8, XREAL_1:7;
hence p1 `2 <= p `2 ; ::_thesis: p `2 <= p2 `2
0 <= 1 - lambda by A5, XREAL_1:48;
then (1 - lambda) * (p1 `2) <= (1 - lambda) * (p2 `2) by A1, XREAL_1:64;
then p `2 <= ((1 - lambda) * (p2 `2)) + (lambda * (p2 `2)) by A8, XREAL_1:6;
hence p `2 <= p2 `2 ; ::_thesis: verum
end;
theorem Th5: :: TOPREAL1:5
for n being Nat
for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) holds
LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2))
proof
let n be Nat; ::_thesis: for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) holds
LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2))
let p, p1, p2 be Point of (TOP-REAL n); ::_thesis: ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) )
now__::_thesis:_(_p_in_LSeg_(p1,p2)_&_p_in_LSeg_(p1,p2)_implies_LSeg_(p1,p2)_=_(LSeg_(p1,p))_\/_(LSeg_(p,p2))_)
assume A1: p in LSeg (p1,p2) ; ::_thesis: ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) )
then consider r being Real such that
A2: p = ((1 - r) * p1) + (r * p2) and
A3: 0 <= r and
A4: r <= 1 ;
now__::_thesis:_(_p_in_LSeg_(p1,p2)_implies_LSeg_(p1,p2)_=_(LSeg_(p1,p))_\/_(LSeg_(p,p2))_)
percases ( ( 0 <> r & r <> 1 ) or not 0 <> r or not r <> 1 ) ;
supposeA5: ( 0 <> r & r <> 1 ) ; ::_thesis: ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) )
now__::_thesis:_for_q_being_set_st_q_in_LSeg_(p1,p2)_holds_
q_in_(LSeg_(p1,p))_\/_(LSeg_(p,p2))
let q be set ; ::_thesis: ( q in LSeg (p1,p2) implies q in (LSeg (p1,p)) \/ (LSeg (p,p2)) )
assume q in LSeg (p1,p2) ; ::_thesis: q in (LSeg (p1,p)) \/ (LSeg (p,p2))
then consider b being Real such that
A6: q = ((1 - b) * p1) + (b * p2) and
A7: 0 <= b and
A8: b <= 1 ;
now__::_thesis:_q_in_(LSeg_(p1,p))_\/_(LSeg_(p,p2))
percases ( b <= r or not b <= r ) ;
supposeA9: b <= r ; ::_thesis: q in (LSeg (p1,p)) \/ (LSeg (p,p2))
set x = b * (1 / r);
b * (1 / r) <= r * (1 / r) by A3, A9, XREAL_1:64;
then A10: b * (1 / r) <= 1 by A5, XCMPLX_1:106;
((1 - (b * (1 / r))) * p1) + ((b * (1 / r)) * p) = ((1 - (b * (1 / r))) * p1) + (((b * (1 / r)) * ((1 - r) * p1)) + ((b * (1 / r)) * (r * p2))) by A2, EUCLID:32
.= (((1 - (b * (1 / r))) * p1) + ((b * (1 / r)) * ((1 - r) * p1))) + ((b * (1 / r)) * (r * p2)) by EUCLID:26
.= (((1 - (b * (1 / r))) * p1) + (((b * (1 / r)) * (1 - r)) * p1)) + ((b * (1 / r)) * (r * p2)) by EUCLID:30
.= (((1 - (b * (1 / r))) * p1) + (((b * (1 / r)) * (1 - r)) * p1)) + (((b * (1 / r)) * r) * p2) by EUCLID:30
.= (((1 - (b * (1 / r))) + ((b * (1 / r)) * (1 - r))) * p1) + (((b * (1 / r)) * r) * p2) by EUCLID:33
.= ((1 - ((b * (1 / r)) * r)) * p1) + (b * p2) by A5, XCMPLX_1:109
.= q by A5, A6, XCMPLX_1:109 ;
then q in { (((1 - lambda) * p1) + (lambda * p)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } by A3, A7, A10;
hence q in (LSeg (p1,p)) \/ (LSeg (p,p2)) by XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA11: not b <= r ; ::_thesis: q in (LSeg (p1,p)) \/ (LSeg (p,p2))
set bp = 1 - b;
set rp = 1 - r;
set x = (1 - b) * (1 / (1 - r));
A12: 0 <> 1 - r by A5;
r - r = 0 ;
then A13: 0 <= 1 - r by A4, XREAL_1:9;
1 - b <= 1 - r by A11, XREAL_1:10;
then (1 - b) * (1 / (1 - r)) <= (1 - r) * (1 / (1 - r)) by A13, XREAL_1:64;
then A14: (1 - b) * (1 / (1 - r)) <= 1 by A12, XCMPLX_1:106;
A15: 0 <= 1 - b by A8, XREAL_1:48;
A16: 1 - 0 = 1 ;
((1 - ((1 - b) * (1 / (1 - r)))) * p2) + (((1 - b) * (1 / (1 - r))) * p) = ((1 - ((1 - b) * (1 / (1 - r)))) * p2) + ((((1 - b) * (1 / (1 - r))) * ((1 - (1 - r)) * p2)) + (((1 - b) * (1 / (1 - r))) * ((1 - r) * p1))) by A2, EUCLID:32
.= (((1 - ((1 - b) * (1 / (1 - r)))) * p2) + (((1 - b) * (1 / (1 - r))) * ((1 - (1 - r)) * p2))) + (((1 - b) * (1 / (1 - r))) * ((1 - r) * p1)) by EUCLID:26
.= (((1 - ((1 - b) * (1 / (1 - r)))) * p2) + ((((1 - b) * (1 / (1 - r))) * (1 - (1 - r))) * p2)) + (((1 - b) * (1 / (1 - r))) * ((1 - r) * p1)) by EUCLID:30
.= (((1 - ((1 - b) * (1 / (1 - r)))) * p2) + ((((1 - b) * (1 / (1 - r))) * (1 - (1 - r))) * p2)) + ((((1 - b) * (1 / (1 - r))) * (1 - r)) * p1) by EUCLID:30
.= (((1 - ((1 - b) * (1 / (1 - r)))) + (((1 - b) * (1 / (1 - r))) * (1 - (1 - r)))) * p2) + ((((1 - b) * (1 / (1 - r))) * (1 - r)) * p1) by EUCLID:33
.= ((1 - (((1 - b) * (1 / (1 - r))) * (1 - r))) * p2) + ((1 - b) * p1) by A5, A16, XCMPLX_1:109
.= ((1 - (1 - b)) * p2) + ((1 - b) * p1) by A12, XCMPLX_1:109
.= q by A6 ;
then q in { (((1 - lambda) * p2) + (lambda * p)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } by A15, A13, A14;
then q in LSeg (p,p2) by RLTOPSP1:def_2;
hence q in (LSeg (p1,p)) \/ (LSeg (p,p2)) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence q in (LSeg (p1,p)) \/ (LSeg (p,p2)) ; ::_thesis: verum
end;
then A17: LSeg (p1,p2) c= (LSeg (p1,p)) \/ (LSeg (p,p2)) by TARSKI:def_3;
A18: LSeg (p,p2) c= LSeg (p1,p2) by A1, Lm1;
LSeg (p1,p) c= LSeg (p1,p2) by A1, Lm1;
then (LSeg (p1,p)) \/ (LSeg (p,p2)) c= LSeg (p1,p2) by A18, XBOOLE_1:8;
hence ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) ) by A17, XBOOLE_0:def_10; ::_thesis: verum
end;
supposeA19: ( not 0 <> r or not r <> 1 ) ; ::_thesis: ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) )
now__::_thesis:_LSeg_(p1,p2)_=_(LSeg_(p1,p))_\/_(LSeg_(p,p2))
percases ( r = 0 or r = 1 ) by A19;
supposeA20: r = 0 ; ::_thesis: LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2))
A21: p in LSeg (p,p2) by RLTOPSP1:68;
A22: p = (1 * p1) + (0. (TOP-REAL n)) by A2, A20, EUCLID:29
.= p1 + (0. (TOP-REAL n)) by EUCLID:29
.= p1 by EUCLID:27 ;
then LSeg (p1,p) = {p} by RLTOPSP1:70;
then LSeg (p1,p) c= LSeg (p,p2) by A21, ZFMISC_1:31;
hence LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) by A22, XBOOLE_1:12; ::_thesis: verum
end;
supposeA23: r = 1 ; ::_thesis: LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2))
A24: p in LSeg (p1,p) by RLTOPSP1:68;
A25: p = (0. (TOP-REAL n)) + (1 * p2) by A2, A23, EUCLID:29
.= (0. (TOP-REAL n)) + p2 by EUCLID:29
.= p2 by EUCLID:27 ;
then LSeg (p,p2) = {p} by RLTOPSP1:70;
then LSeg (p,p2) c= LSeg (p1,p) by A24, ZFMISC_1:31;
hence LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) by A25, XBOOLE_1:12; ::_thesis: verum
end;
end;
end;
hence ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) ) ; ::_thesis: verum
end;
end;
end;
hence ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) ) ; ::_thesis: verum
end;
hence ( p in LSeg (p1,p2) implies LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) ) ; ::_thesis: verum
end;
theorem Th6: :: TOPREAL1:6
for n being Nat
for p1, p2, q1, q2 being Point of (TOP-REAL n) st q1 in LSeg (p1,p2) & q2 in LSeg (p1,p2) holds
LSeg (q1,q2) c= LSeg (p1,p2)
proof
let n be Nat; ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL n) st q1 in LSeg (p1,p2) & q2 in LSeg (p1,p2) holds
LSeg (q1,q2) c= LSeg (p1,p2)
let p1, p2, q1, q2 be Point of (TOP-REAL n); ::_thesis: ( q1 in LSeg (p1,p2) & q2 in LSeg (p1,p2) implies LSeg (q1,q2) c= LSeg (p1,p2) )
assume that
A1: q1 in LSeg (p1,p2) and
A2: q2 in LSeg (p1,p2) ; ::_thesis: LSeg (q1,q2) c= LSeg (p1,p2)
A3: LSeg (p1,p2) = (LSeg (p1,q1)) \/ (LSeg (q1,p2)) by A1, Th5;
now__::_thesis:_LSeg_(q1,q2)_c=_LSeg_(p1,p2)
percases ( q2 in LSeg (p1,q1) or q2 in LSeg (q1,p2) ) by A2, A3, XBOOLE_0:def_3;
supposeA4: q2 in LSeg (p1,q1) ; ::_thesis: LSeg (q1,q2) c= LSeg (p1,p2)
A5: LSeg (p1,q1) c= LSeg (p1,p2) by A1, Lm1;
LSeg (q2,q1) c= LSeg (p1,q1) by A4, Lm1;
hence LSeg (q1,q2) c= LSeg (p1,p2) by A5, XBOOLE_1:1; ::_thesis: verum
end;
supposeA6: q2 in LSeg (q1,p2) ; ::_thesis: LSeg (q1,q2) c= LSeg (p1,p2)
A7: LSeg (q1,p2) c= LSeg (p1,p2) by A1, Lm1;
LSeg (q1,q2) c= LSeg (q1,p2) by A6, Lm1;
hence LSeg (q1,q2) c= LSeg (p1,p2) by A7, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
hence LSeg (q1,q2) c= LSeg (p1,p2) ; ::_thesis: verum
end;
theorem :: TOPREAL1:7
for n being Nat
for p, q, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) & q in LSeg (p1,p2) holds
LSeg (p1,p2) = ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2))
proof
let n be Nat; ::_thesis: for p, q, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) & q in LSeg (p1,p2) holds
LSeg (p1,p2) = ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2))
let p, q, p1, p2 be Point of (TOP-REAL n); ::_thesis: ( p in LSeg (p1,p2) & q in LSeg (p1,p2) implies LSeg (p1,p2) = ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2)) )
assume that
A1: p in LSeg (p1,p2) and
A2: q in LSeg (p1,p2) ; ::_thesis: LSeg (p1,p2) = ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2))
A3: LSeg (p,q) c= LSeg (p1,p2) by A1, A2, Th6;
A4: LSeg (p1,p2) = (LSeg (p1,q)) \/ (LSeg (q,p2)) by A2, Th5;
A5: now__::_thesis:_LSeg_(p1,p2)_c=_((LSeg_(p1,p))_\/_(LSeg_(p,q)))_\/_(LSeg_(q,p2))
percases ( p in LSeg (p1,q) or not p in LSeg (p1,q) ) ;
suppose p in LSeg (p1,q) ; ::_thesis: LSeg (p1,p2) c= ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2))
hence LSeg (p1,p2) c= ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2)) by A4, Th5; ::_thesis: verum
end;
suppose not p in LSeg (p1,q) ; ::_thesis: LSeg (p1,p2) c= ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2))
then p in LSeg (q,p2) by A1, A4, XBOOLE_0:def_3;
then A6: LSeg (q,p2) = (LSeg (q,p)) \/ (LSeg (p,p2)) by Th5;
LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2)) by A1, Th5;
then A7: LSeg (p1,p2) c= (LSeg (p1,p)) \/ (LSeg (q,p2)) by A6, XBOOLE_1:7, XBOOLE_1:9;
A8: ((LSeg (p1,p)) \/ (LSeg (q,p2))) \/ (LSeg (p,q)) = ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2)) by XBOOLE_1:4;
(LSeg (p1,p)) \/ (LSeg (q,p2)) c= ((LSeg (p1,p)) \/ (LSeg (q,p2))) \/ (LSeg (p,q)) by XBOOLE_1:7;
hence LSeg (p1,p2) c= ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2)) by A7, A8, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
p1 in LSeg (p1,p2) by RLTOPSP1:68;
then LSeg (p1,p) c= LSeg (p1,p2) by A1, Th6;
then A9: (LSeg (p1,p)) \/ (LSeg (p,q)) c= LSeg (p1,p2) by A3, XBOOLE_1:8;
p2 in LSeg (p1,p2) by RLTOPSP1:68;
then LSeg (q,p2) c= LSeg (p1,p2) by A2, Th6;
then ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2)) c= LSeg (p1,p2) by A9, XBOOLE_1:8;
hence LSeg (p1,p2) = ((LSeg (p1,p)) \/ (LSeg (p,q))) \/ (LSeg (q,p2)) by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: TOPREAL1:8
for n being Nat
for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) holds
(LSeg (p1,p)) /\ (LSeg (p,p2)) = {p}
proof
let n be Nat; ::_thesis: for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) holds
(LSeg (p1,p)) /\ (LSeg (p,p2)) = {p}
let p, p1, p2 be Point of (TOP-REAL n); ::_thesis: ( p in LSeg (p1,p2) implies (LSeg (p1,p)) /\ (LSeg (p,p2)) = {p} )
A1: p in LSeg (p,p2) by RLTOPSP1:68;
assume A2: p in LSeg (p1,p2) ; ::_thesis: (LSeg (p1,p)) /\ (LSeg (p,p2)) = {p}
A3: now__::_thesis:_(LSeg_(p1,p))_/\_(LSeg_(p,p2))_c=_{p}
assume not (LSeg (p1,p)) /\ (LSeg (p,p2)) c= {p} ; ::_thesis: contradiction
then consider y being set such that
A4: y in (LSeg (p1,p)) /\ (LSeg (p,p2)) and
A5: not y in {p} by TARSKI:def_3;
reconsider q = y as Point of (TOP-REAL n) by A4;
A6: q in LSeg (p1,p) by A4, XBOOLE_0:def_4;
then consider d being Real such that
A7: q = ((1 - d) * p1) + (d * p) and
0 <= d and
A8: d <= 1 ;
q in LSeg (p,p2) by A4, XBOOLE_0:def_4;
then consider e being Real such that
A9: q = ((1 - e) * p) + (e * p2) and
A10: 0 <= e and
e <= 1 ;
consider a being Real such that
A11: p = ((1 - a) * p1) + (a * p2) and
A12: 0 <= a and
A13: a <= 1 by A2;
A14: 1 - a >= 0 by A13, XREAL_1:48;
now__::_thesis:_not_d_=_1
assume d = 1 ; ::_thesis: contradiction
then q = ((1 - 1) * p1) + p by A7, EUCLID:29
.= (0. (TOP-REAL n)) + p by EUCLID:29
.= p by EUCLID:27 ;
hence contradiction by A5, TARSKI:def_1; ::_thesis: verum
end;
then d < 1 by A8, XXREAL_0:1;
then A15: 1 - d > 0 by XREAL_1:50;
now__::_thesis:_not_a_=_0
assume a = 0 ; ::_thesis: contradiction
then p = ((1 - 0) * p1) + (0. (TOP-REAL n)) by A11, EUCLID:29
.= (1 - 0) * p1 by EUCLID:27
.= p1 by EUCLID:29 ;
hence contradiction by A5, A6, RLTOPSP1:70; ::_thesis: verum
end;
then A16: (1 - d) * a > 0 by A12, A15, XREAL_1:129;
set f = ((1 - e) * a) + e;
q = (((1 - e) * ((1 - a) * p1)) + ((1 - e) * (a * p2))) + (e * p2) by A11, A9, EUCLID:32
.= ((((1 - e) * (1 - a)) * p1) + ((1 - e) * (a * p2))) + (e * p2) by EUCLID:30
.= ((((1 - e) * (1 - a)) * p1) + (((1 - e) * a) * p2)) + (e * p2) by EUCLID:30
.= (((1 - e) * (1 - a)) * p1) + ((((1 - e) * a) * p2) + (e * p2)) by EUCLID:26
.= (((1 - e) * (1 - a)) * p1) + ((((1 - e) * a) + e) * p2) by EUCLID:33 ;
then A17: p - q = ((((1 - a) * p1) + (a * p2)) - ((1 - (((1 - e) * a) + e)) * p1)) - ((((1 - e) * a) + e) * p2) by A11, EUCLID:46
.= ((((1 - a) * p1) - ((1 - (((1 - e) * a) + e)) * p1)) + (a * p2)) - ((((1 - e) * a) + e) * p2) by EUCLID:45
.= ((((1 - a) - (1 - (((1 - e) * a) + e))) * p1) + (a * p2)) - ((((1 - e) * a) + e) * p2) by EUCLID:50
.= ((((((1 - e) * a) + e) - a) * p1) - ((((1 - e) * a) + e) * p2)) + (a * p2) by EUCLID:45
.= (((((1 - e) * a) + e) - a) * p1) - (((((1 - e) * a) + e) * p2) - (a * p2)) by EUCLID:47
.= (((((1 - e) * a) + e) - a) * p1) - (((((1 - e) * a) + e) - a) * p2) by EUCLID:50
.= ((((1 - e) * a) + e) - a) * (p1 - p2) by EUCLID:49 ;
q = ((1 - d) * p1) + ((d * ((1 - a) * p1)) + (d * (a * p2))) by A11, A7, EUCLID:32
.= (((1 - d) * p1) + (d * ((1 - a) * p1))) + (d * (a * p2)) by EUCLID:26
.= (((1 - d) * p1) + ((d * (1 - a)) * p1)) + (d * (a * p2)) by EUCLID:30
.= (((1 - d) + (d * (1 - a))) * p1) + (d * (a * p2)) by EUCLID:33
.= ((1 - (d * a)) * p1) + ((d * a) * p2) by EUCLID:30 ;
then p - q = ((((1 - a) * p1) + (a * p2)) - ((1 - (d * a)) * p1)) - ((d * a) * p2) by A11, EUCLID:46
.= ((((1 - a) * p1) - ((1 - (d * a)) * p1)) + (a * p2)) - ((d * a) * p2) by EUCLID:45
.= ((((1 - a) - (1 - (d * a))) * p1) + (a * p2)) - ((d * a) * p2) by EUCLID:50
.= ((((d * a) - a) * p1) - ((d * a) * p2)) + (a * p2) by EUCLID:45
.= (((d * a) - a) * p1) - (((d * a) * p2) - (a * p2)) by EUCLID:47
.= (((d * a) - a) * p1) - (((d * a) - a) * p2) by EUCLID:50
.= ((d * a) - a) * (p1 - p2) by EUCLID:49 ;
then (((((1 - e) * a) + e) - a) * (p1 - p2)) - (((d * a) - a) * (p1 - p2)) = 0. (TOP-REAL n) by A17, EUCLID:42;
then (((((1 - e) * a) + e) - a) - ((d * a) - a)) * (p1 - p2) = 0. (TOP-REAL n) by EUCLID:50;
then A18: ( (((1 - e) * a) + e) - (d * a) = 0 or p1 - p2 = 0. (TOP-REAL n) ) by EUCLID:31;
(((1 - e) * a) + e) - (d * a) = ((1 - d) * a) + (e * (1 - a)) ;
then p1 = p2 by A10, A18, A16, A14, EUCLID:43;
then p in {p1} by A2, RLTOPSP1:70;
then p = p1 by TARSKI:def_1;
hence contradiction by A5, A6, RLTOPSP1:70; ::_thesis: verum
end;
p in LSeg (p1,p) by RLTOPSP1:68;
then p in (LSeg (p1,p)) /\ (LSeg (p,p2)) by A1, XBOOLE_0:def_4;
then {p} c= (LSeg (p1,p)) /\ (LSeg (p,p2)) by ZFMISC_1:31;
hence (LSeg (p1,p)) /\ (LSeg (p,p2)) = {p} by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
Lm2: for T being TopSpace holds
( T is T_2 iff TopStruct(# the carrier of T, the topology of T #) is T_2 )
proof
let T be TopSpace; ::_thesis: ( T is T_2 iff TopStruct(# the carrier of T, the topology of T #) is T_2 )
thus ( T is T_2 implies TopStruct(# the carrier of T, the topology of T #) is T_2 ) ::_thesis: ( TopStruct(# the carrier of T, the topology of T #) is T_2 implies T is T_2 )
proof
assume A1: T is T_2 ; ::_thesis: TopStruct(# the carrier of T, the topology of T #) is T_2
let p, q be Point of TopStruct(# the carrier of T, the topology of T #); :: according to PRE_TOPC:def_10 ::_thesis: ( p = q or ex b1, b2 being Element of K10( the carrier of TopStruct(# the carrier of T, the topology of T #)) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) )
assume A2: p <> q ; ::_thesis: ex b1, b2 being Element of K10( the carrier of TopStruct(# the carrier of T, the topology of T #)) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
reconsider pp = p, qq = q as Point of T ;
consider G1, G2 being Subset of T such that
A3: G1 is open and
A4: G2 is open and
A5: pp in G1 and
A6: qq in G2 and
A7: G1 misses G2 by A1, A2, PRE_TOPC:def_10;
reconsider H1 = G1, H2 = G2 as Subset of TopStruct(# the carrier of T, the topology of T #) ;
take H1 ; ::_thesis: ex b1 being Element of K10( the carrier of TopStruct(# the carrier of T, the topology of T #)) st
( H1 is open & b1 is open & p in H1 & q in b1 & H1 misses b1 )
take H2 ; ::_thesis: ( H1 is open & H2 is open & p in H1 & q in H2 & H1 misses H2 )
thus ( H1 is open & H2 is open ) by A3, A4, PRE_TOPC:30; ::_thesis: ( p in H1 & q in H2 & H1 misses H2 )
thus ( p in H1 & q in H2 & H1 misses H2 ) by A5, A6, A7; ::_thesis: verum
end;
assume A8: TopStruct(# the carrier of T, the topology of T #) is T_2 ; ::_thesis: T is T_2
let p, q be Point of T; :: according to PRE_TOPC:def_10 ::_thesis: ( p = q or ex b1, b2 being Element of K10( the carrier of T) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) )
assume A9: p <> q ; ::_thesis: ex b1, b2 being Element of K10( the carrier of T) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
reconsider pp = p, qq = q as Point of TopStruct(# the carrier of T, the topology of T #) ;
consider G1, G2 being Subset of TopStruct(# the carrier of T, the topology of T #) such that
A10: G1 is open and
A11: G2 is open and
A12: pp in G1 and
A13: qq in G2 and
A14: G1 misses G2 by A8, A9, PRE_TOPC:def_10;
reconsider H1 = G1, H2 = G2 as Subset of T ;
take H1 ; ::_thesis: ex b1 being Element of K10( the carrier of T) st
( H1 is open & b1 is open & p in H1 & q in b1 & H1 misses b1 )
take H2 ; ::_thesis: ( H1 is open & H2 is open & p in H1 & q in H2 & H1 misses H2 )
thus ( H1 is open & H2 is open ) by A10, A11, PRE_TOPC:30; ::_thesis: ( p in H1 & q in H2 & H1 misses H2 )
thus ( p in H1 & q in H2 & H1 misses H2 ) by A12, A13, A14; ::_thesis: verum
end;
registration
let n be Nat;
cluster the carrier of (TOP-REAL n) -> functional ;
coherence
the carrier of (TOP-REAL n) is functional
proof
let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in the carrier of (TOP-REAL n) or x is set )
thus ( not x in the carrier of (TOP-REAL n) or x is set ) by EUCLID:23; ::_thesis: verum
end;
end;
theorem Th9: :: TOPREAL1:9
for n being Nat
for p1, p2 being Point of (TOP-REAL n) st p1 <> p2 holds
LSeg (p1,p2) is_an_arc_of p1,p2
proof
let n be Nat; ::_thesis: for p1, p2 being Point of (TOP-REAL n) st p1 <> p2 holds
LSeg (p1,p2) is_an_arc_of p1,p2
let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( p1 <> p2 implies LSeg (p1,p2) is_an_arc_of p1,p2 )
set P = LSeg (p1,p2);
reconsider PP = LSeg (p1,p2) as Subset of (Euclid n) by EUCLID:67;
not PP is empty ;
then reconsider PP = LSeg (p1,p2) as non empty Subset of (Euclid n) ;
reconsider p19 = p1, p29 = p2 as Element of REAL n by EUCLID:22;
defpred S1[ set , set ] means for x being Real st x = $1 holds
$2 = ((1 - x) * p1) + (x * p2);
A1: [#] I[01] = [.0,1.] by BORSUK_1:40;
A2: for a being set st a in [.0,1.] holds
ex u being set st S1[a,u]
proof
let a be set ; ::_thesis: ( a in [.0,1.] implies ex u being set st S1[a,u] )
assume a in [.0,1.] ; ::_thesis: ex u being set st S1[a,u]
then reconsider x = a as Real ;
take ((1 - x) * p1) + (x * p2) ; ::_thesis: S1[a,((1 - x) * p1) + (x * p2)]
thus S1[a,((1 - x) * p1) + (x * p2)] ; ::_thesis: verum
end;
consider f being Function such that
A3: dom f = [.0,1.] and
A4: for a being set st a in [.0,1.] holds
S1[a,f . a] from CLASSES1:sch_1(A2);
A5: rng f c= the carrier of ((TOP-REAL n) | (LSeg (p1,p2)))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in the carrier of ((TOP-REAL n) | (LSeg (p1,p2))) )
assume y in rng f ; ::_thesis: y in the carrier of ((TOP-REAL n) | (LSeg (p1,p2)))
then consider x being set such that
A6: x in dom f and
A7: y = f . x by FUNCT_1:def_3;
x in { r where r is Real : ( 0 <= r & r <= 1 ) } by A3, A6, RCOMP_1:def_1;
then consider r being Real such that
A8: r = x and
A9: 0 <= r and
A10: r <= 1 ;
y = ((1 - r) * p1) + (r * p2) by A3, A4, A6, A7, A8;
then y in { (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } by A9, A10;
then y in [#] ((TOP-REAL n) | (LSeg (p1,p2))) by PRE_TOPC:def_5;
hence y in the carrier of ((TOP-REAL n) | (LSeg (p1,p2))) ; ::_thesis: verum
end;
then reconsider f = f as Function of I[01],((TOP-REAL n) | (LSeg (p1,p2))) by A3, BORSUK_1:40, FUNCT_2:def_1, RELSET_1:4;
A11: I[01] is compact by HEINE:4, TOPMETR:20;
assume A12: p1 <> p2 ; ::_thesis: LSeg (p1,p2) is_an_arc_of p1,p2
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_f_&_x2_in_dom_f_&_f_._x1_=_f_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A13: x1 in dom f and
A14: x2 in dom f and
A15: f . x1 = f . x2 ; ::_thesis: x1 = x2
x2 in { r where r is Real : ( 0 <= r & r <= 1 ) } by A3, A14, RCOMP_1:def_1;
then consider r2 being Real such that
A16: r2 = x2 and
0 <= r2 and
r2 <= 1 ;
A17: f . x2 = ((1 - r2) * p1) + (r2 * p2) by A3, A4, A14, A16;
x1 in { r where r is Real : ( 0 <= r & r <= 1 ) } by A3, A13, RCOMP_1:def_1;
then consider r1 being Real such that
A18: r1 = x1 and
0 <= r1 and
r1 <= 1 ;
f . x1 = ((1 - r1) * p1) + (r1 * p2) by A3, A4, A13, A18;
then (((1 - r1) * p1) + (r1 * p2)) + ((- r1) * p2) = ((1 - r2) * p1) + ((r2 * p2) + ((- r1) * p2)) by A15, A17, EUCLID:26;
then (((1 - r1) * p1) + (r1 * p2)) + ((- r1) * p2) = ((1 - r2) * p1) + ((r2 + (- r1)) * p2) by EUCLID:33;
then ((1 - r1) * p1) + ((r1 * p2) + ((- r1) * p2)) = ((1 - r2) * p1) + ((r2 - r1) * p2) by EUCLID:26;
then ((1 - r1) * p1) + ((r1 + (- r1)) * p2) = ((1 - r2) * p1) + ((r2 - r1) * p2) by EUCLID:33;
then ((1 - r1) * p1) + (0. (TOP-REAL n)) = ((1 - r2) * p1) + ((r2 - r1) * p2) by EUCLID:29;
then ((- (1 - r2)) * p1) + ((1 - r1) * p1) = ((- (1 - r2)) * p1) + (((1 - r2) * p1) + ((r2 - r1) * p2)) by EUCLID:27;
then ((- (1 - r2)) * p1) + ((1 - r1) * p1) = (((- (1 - r2)) * p1) + ((1 - r2) * p1)) + ((r2 - r1) * p2) by EUCLID:26;
then ((- (1 - r2)) * p1) + ((1 - r1) * p1) = (((- (1 - r2)) + (1 - r2)) * p1) + ((r2 - r1) * p2) by EUCLID:33;
then ((- (1 - r2)) * p1) + ((1 - r1) * p1) = (0. (TOP-REAL n)) + ((r2 - r1) * p2) by EUCLID:29;
then ((- (1 - r2)) * p1) + ((1 - r1) * p1) = (r2 - r1) * p2 by EUCLID:27;
then ((r2 - 1) + (1 - r1)) * p1 = (r2 - r1) * p2 by EUCLID:33;
then r2 - r1 = 0 by A12, EUCLID:34;
hence x1 = x2 by A18, A16; ::_thesis: verum
end;
then A19: f is one-to-one by FUNCT_1:def_4;
[#] ((TOP-REAL n) | (LSeg (p1,p2))) c= rng f
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in [#] ((TOP-REAL n) | (LSeg (p1,p2))) or a in rng f )
assume a in [#] ((TOP-REAL n) | (LSeg (p1,p2))) ; ::_thesis: a in rng f
then a in LSeg (p1,p2) by PRE_TOPC:def_5;
then consider lambda being Real such that
A20: a = ((1 - lambda) * p1) + (lambda * p2) and
A21: 0 <= lambda and
A22: lambda <= 1 ;
lambda in { r where r is Real : ( 0 <= r & r <= 1 ) } by A21, A22;
then A23: lambda in dom f by A3, RCOMP_1:def_1;
then a = f . lambda by A3, A4, A20;
hence a in rng f by A23, FUNCT_1:def_3; ::_thesis: verum
end;
then A24: rng f = [#] ((TOP-REAL n) | (LSeg (p1,p2))) by A5, XBOOLE_0:def_10;
A25: TopSpaceMetr (Euclid n) is T_2 by PCOMPS_1:34;
A26: (TOP-REAL n) | (LSeg (p1,p2)) = TopSpaceMetr ((Euclid n) | PP) by EUCLID:63;
for W being Point of I[01]
for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G
proof
reconsider p11 = p1, p22 = p2 as Point of (Euclid n) by EUCLID:67;
let W be Point of I[01]; ::_thesis: for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G
let G be a_neighborhood of f . W; ::_thesis: ex H being a_neighborhood of W st f .: H c= G
reconsider W9 = W as Point of (Closed-Interval-MSpace (0,1)) by BORSUK_1:40, TOPMETR:10;
A27: (Pitag_dist n) . (p19,p29) = dist (p11,p22) by METRIC_1:def_1;
[#] ((TOP-REAL n) | (LSeg (p1,p2))) = LSeg (p1,p2) by PRE_TOPC:def_5;
then reconsider Y = f . W as Point of ((Euclid n) | PP) by TOPMETR:def_2;
A28: dist (p11,p22) >= 0 by METRIC_1:5;
reconsider W1 = W as Real by BORSUK_1:40, TARSKI:def_3;
LSeg (p1,p2) = the carrier of ((Euclid n) | PP) by TOPMETR:def_2;
then reconsider WW9 = Y as Point of (Euclid n) by TARSKI:def_3;
f . W in Int G by CONNSP_2:def_1;
then consider Q being Subset of ((TOP-REAL n) | (LSeg (p1,p2))) such that
A29: Q is open and
A30: Q c= G and
A31: f . W in Q by TOPS_1:22;
consider r being real number such that
A32: r > 0 and
A33: Ball (Y,r) c= Q by A26, A29, A31, TOPMETR:15;
reconsider r = r as Element of REAL by XREAL_0:def_1;
set delta = r / ((Pitag_dist n) . (p19,p29));
reconsider H = Ball (W9,(r / ((Pitag_dist n) . (p19,p29)))) as Subset of I[01] by BORSUK_1:40, TOPMETR:10;
Closed-Interval-TSpace (0,1) = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:def_7;
then A34: H is open by TOPMETR:14, TOPMETR:20;
A35: dist (p11,p22) <> 0 by A12, METRIC_1:2;
then W in H by A32, A27, A28, TBSP_1:11, XREAL_1:139;
then W in Int H by A34, TOPS_1:23;
then reconsider H = H as a_neighborhood of W by CONNSP_2:def_1;
take H ; ::_thesis: f .: H c= G
A36: r / ((Pitag_dist n) . (p19,p29)) > 0 by A32, A27, A28, A35, XREAL_1:139;
f .: H c= Ball (Y,r)
proof
reconsider WW1 = WW9 as Element of REAL n ;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in f .: H or a in Ball (Y,r) )
A37: rng f c= the carrier of ((TOP-REAL n) | (LSeg (p1,p2))) by RELAT_1:def_19;
assume a in f .: H ; ::_thesis: a in Ball (Y,r)
then consider u being set such that
A38: u in dom f and
A39: u in H and
A40: a = f . u by FUNCT_1:def_6;
reconsider u1 = u as Real by A3, A38;
A41: [#] ((TOP-REAL n) | (LSeg (p1,p2))) = LSeg (p1,p2) by PRE_TOPC:def_5;
reconsider u9 = u as Point of (Closed-Interval-MSpace (0,1)) by A39;
reconsider W99 = W9, u99 = u9 as Point of RealSpace by TOPMETR:8;
A42: dist (W9,u9) = the distance of (Closed-Interval-MSpace (0,1)) . (W9,u9) by METRIC_1:def_1
.= the distance of RealSpace . (W99,u99) by TOPMETR:def_1
.= dist (W99,u99) by METRIC_1:def_1 ;
dist (W9,u9) < r / ((Pitag_dist n) . (p19,p29)) by A39, METRIC_1:11;
then abs (W1 - u1) < r / ((Pitag_dist n) . (p19,p29)) by A42, TOPMETR:11;
then abs (- (u1 - W1)) < r / ((Pitag_dist n) . (p19,p29)) ;
then A43: abs (u1 - W1) < r / ((Pitag_dist n) . (p19,p29)) by COMPLEX1:52;
A44: r / ((Pitag_dist n) . (p19,p29)) <> 0 by A32, A27, A28, A35, XREAL_1:139;
then (Pitag_dist n) . (p19,p29) = r / (r / ((Pitag_dist n) . (p19,p29))) by XCMPLX_1:54;
then A45: |.(p19 - p29).| = r / (r / ((Pitag_dist n) . (p19,p29))) by EUCLID:def_6;
f . u in rng f by A38, FUNCT_1:def_3;
then reconsider aa = a as Point of ((Euclid n) | PP) by A40, A37, A41, TOPMETR:def_2;
LSeg (p1,p2) = the carrier of ((Euclid n) | PP) by TOPMETR:def_2;
then reconsider aa9 = aa as Point of (Euclid n) by TARSKI:def_3;
reconsider aa1 = aa9 as Element of REAL n ;
A46: p19 - p29 = p1 - p2 by EUCLID:69;
A47: WW1 = ((1 - W1) * p1) + (W1 * p2) by A4, BORSUK_1:40;
aa1 = ((1 - u1) * p1) + (u1 * p2) by A3, A4, A38, A40;
then WW1 - aa1 = (((1 - W1) * p1) + (W1 * p2)) - (((1 - u1) * p1) + (u1 * p2)) by A47, EUCLID:69
.= (((W1 * p2) + ((1 - W1) * p1)) - ((1 - u1) * p1)) - (u1 * p2) by EUCLID:46
.= ((W1 * p2) + (((1 - W1) * p1) - ((1 - u1) * p1))) - (u1 * p2) by EUCLID:45
.= ((W1 * p2) + (((1 - W1) - (1 - u1)) * p1)) - (u1 * p2) by EUCLID:50
.= ((u1 - W1) * p1) + ((W1 * p2) - (u1 * p2)) by EUCLID:45
.= ((u1 - W1) * p1) + ((W1 - u1) * p2) by EUCLID:50
.= ((u1 - W1) * p1) + ((- (u1 - W1)) * p2)
.= ((u1 - W1) * p1) + (- ((u1 - W1) * p2)) by EUCLID:40
.= ((u1 - W1) * p1) - ((u1 - W1) * p2) by EUCLID:41
.= (u1 - W1) * (p1 - p2) by EUCLID:49
.= (u1 - W1) * (p19 - p29) by A46, EUCLID:65 ;
then A48: |.(WW1 - aa1).| = (abs (u1 - W1)) * |.(p19 - p29).| by EUCLID:11;
r / (r / ((Pitag_dist n) . (p19,p29))) > 0 by A32, A36, XREAL_1:139;
then |.(WW1 - aa1).| < (r / ((Pitag_dist n) . (p19,p29))) * (r / (r / ((Pitag_dist n) . (p19,p29)))) by A48, A43, A45, XREAL_1:68;
then |.(WW1 - aa1).| < r by A44, XCMPLX_1:87;
then the distance of (Euclid n) . (WW9,aa9) < r by EUCLID:def_6;
then the distance of ((Euclid n) | PP) . (Y,aa) < r by TOPMETR:def_1;
then dist (Y,aa) < r by METRIC_1:def_1;
hence a in Ball (Y,r) by METRIC_1:11; ::_thesis: verum
end;
then f .: H c= Q by A33, XBOOLE_1:1;
hence f .: H c= G by A30, XBOOLE_1:1; ::_thesis: verum
end;
then A49: f is continuous by BORSUK_1:def_1;
take f ; :: according to TOPREAL1:def_1 ::_thesis: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 )
A50: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then reconsider PP = LSeg (p1,p2) as Subset of (TopSpaceMetr (Euclid n)) ;
(TopSpaceMetr (Euclid n)) | PP = (TOP-REAL n) | (LSeg (p1,p2)) by A50, PRE_TOPC:36;
then (TOP-REAL n) | (LSeg (p1,p2)) is T_2 by A25, TOPMETR:2;
hence f is being_homeomorphism by A3, A1, A24, A19, A49, A11, COMPTS_1:17; ::_thesis: ( f . 0 = p1 & f . 1 = p2 )
0 in [.0,1.] by XXREAL_1:1;
hence f . 0 = ((1 - 0) * p1) + (0 * p2) by A4
.= p1 + (0 * p2) by EUCLID:29
.= p1 + (0. (TOP-REAL n)) by EUCLID:29
.= p1 by EUCLID:27 ;
::_thesis: f . 1 = p2
1 in [.0,1.] by XXREAL_1:1;
hence f . 1 = ((1 - 1) * p1) + (1 * p2) by A4
.= (0. (TOP-REAL n)) + (1 * p2) by EUCLID:29
.= 1 * p2 by EUCLID:27
.= p2 by EUCLID:29 ;
::_thesis: verum
end;
registration
let n be Nat;
cluster TOP-REAL n -> T_2 ;
coherence
TOP-REAL n is T_2
proof
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is T_2 by PCOMPS_1:34;
hence TOP-REAL n is T_2 by Lm2; ::_thesis: verum
end;
end;
theorem Th10: :: TOPREAL1:10
for n being Nat
for P being Subset of (TOP-REAL n)
for p1, p2, q1 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & P /\ (LSeg (p2,q1)) = {p2} holds
P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1
proof
let n be Nat; ::_thesis: for P being Subset of (TOP-REAL n)
for p1, p2, q1 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & P /\ (LSeg (p2,q1)) = {p2} holds
P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1
let P be Subset of (TOP-REAL n); ::_thesis: for p1, p2, q1 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & P /\ (LSeg (p2,q1)) = {p2} holds
P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1
let p1, p2, q1 be Point of (TOP-REAL n); ::_thesis: ( P is_an_arc_of p1,p2 & P /\ (LSeg (p2,q1)) = {p2} implies P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 )
assume that
A1: P is_an_arc_of p1,p2 and
A2: P /\ (LSeg (p2,q1)) = {p2} ; ::_thesis: P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1
percases ( p2 <> q1 or p2 = q1 ) ;
suppose p2 <> q1 ; ::_thesis: P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1
then LSeg (p2,q1) is_an_arc_of p2,q1 by Th9;
hence P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 by A1, A2, Th2; ::_thesis: verum
end;
supposeA3: p2 = q1 ; ::_thesis: P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1
then A4: LSeg (p2,q1) = {q1} by RLTOPSP1:70;
q1 in P by A1, A3, Th1;
hence P \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 by A1, A3, A4, ZFMISC_1:40; ::_thesis: verum
end;
end;
end;
theorem Th11: :: TOPREAL1:11
for n being Nat
for P being Subset of (TOP-REAL n)
for p1, p2, q1 being Point of (TOP-REAL n) st P is_an_arc_of p2,p1 & (LSeg (q1,p2)) /\ P = {p2} holds
(LSeg (q1,p2)) \/ P is_an_arc_of q1,p1
proof
let n be Nat; ::_thesis: for P being Subset of (TOP-REAL n)
for p1, p2, q1 being Point of (TOP-REAL n) st P is_an_arc_of p2,p1 & (LSeg (q1,p2)) /\ P = {p2} holds
(LSeg (q1,p2)) \/ P is_an_arc_of q1,p1
let P be Subset of (TOP-REAL n); ::_thesis: for p1, p2, q1 being Point of (TOP-REAL n) st P is_an_arc_of p2,p1 & (LSeg (q1,p2)) /\ P = {p2} holds
(LSeg (q1,p2)) \/ P is_an_arc_of q1,p1
let p1, p2, q1 be Point of (TOP-REAL n); ::_thesis: ( P is_an_arc_of p2,p1 & (LSeg (q1,p2)) /\ P = {p2} implies (LSeg (q1,p2)) \/ P is_an_arc_of q1,p1 )
assume that
A1: P is_an_arc_of p2,p1 and
A2: (LSeg (q1,p2)) /\ P = {p2} ; ::_thesis: (LSeg (q1,p2)) \/ P is_an_arc_of q1,p1
percases ( p2 <> q1 or p2 = q1 ) ;
suppose p2 <> q1 ; ::_thesis: (LSeg (q1,p2)) \/ P is_an_arc_of q1,p1
then LSeg (q1,p2) is_an_arc_of q1,p2 by Th9;
hence (LSeg (q1,p2)) \/ P is_an_arc_of q1,p1 by A1, A2, Th2; ::_thesis: verum
end;
supposeA3: p2 = q1 ; ::_thesis: (LSeg (q1,p2)) \/ P is_an_arc_of q1,p1
then A4: LSeg (q1,p2) = {q1} by RLTOPSP1:70;
q1 in P by A1, A3, Th1;
hence (LSeg (q1,p2)) \/ P is_an_arc_of q1,p1 by A1, A3, A4, ZFMISC_1:40; ::_thesis: verum
end;
end;
end;
theorem :: TOPREAL1:12
for n being Nat
for p1, p2, q1 being Point of (TOP-REAL n) st ( p1 <> p2 or p2 <> q1 ) & (LSeg (p1,p2)) /\ (LSeg (p2,q1)) = {p2} holds
(LSeg (p1,p2)) \/ (LSeg (p2,q1)) is_an_arc_of p1,q1
proof
let n be Nat; ::_thesis: for p1, p2, q1 being Point of (TOP-REAL n) st ( p1 <> p2 or p2 <> q1 ) & (LSeg (p1,p2)) /\ (LSeg (p2,q1)) = {p2} holds
(LSeg (p1,p2)) \/ (LSeg (p2,q1)) is_an_arc_of p1,q1
let p1, p2, q1 be Point of (TOP-REAL n); ::_thesis: ( ( p1 <> p2 or p2 <> q1 ) & (LSeg (p1,p2)) /\ (LSeg (p2,q1)) = {p2} implies (LSeg (p1,p2)) \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 )
assume that
A1: ( p1 <> p2 or p2 <> q1 ) and
A2: (LSeg (p1,p2)) /\ (LSeg (p2,q1)) = {p2} ; ::_thesis: (LSeg (p1,p2)) \/ (LSeg (p2,q1)) is_an_arc_of p1,q1
percases ( p1 <> p2 or p2 <> q1 ) by A1;
suppose p1 <> p2 ; ::_thesis: (LSeg (p1,p2)) \/ (LSeg (p2,q1)) is_an_arc_of p1,q1
hence (LSeg (p1,p2)) \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 by A2, Th9, Th10; ::_thesis: verum
end;
suppose p2 <> q1 ; ::_thesis: (LSeg (p1,p2)) \/ (LSeg (p2,q1)) is_an_arc_of p1,q1
hence (LSeg (p1,p2)) \/ (LSeg (p2,q1)) is_an_arc_of p1,q1 by A2, Th9, Th11; ::_thesis: verum
end;
end;
end;
theorem Th13: :: TOPREAL1:13
( LSeg (|[0,0]|,|[0,1]|) = { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = 0 & p1 `2 <= 1 & p1 `2 >= 0 ) } & LSeg (|[0,1]|,|[1,1]|) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 1 ) } & LSeg (|[0,0]|,|[1,0]|) = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 <= 1 & q1 `1 >= 0 & q1 `2 = 0 ) } & LSeg (|[1,0]|,|[1,1]|) = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = 1 & q2 `2 <= 1 & q2 `2 >= 0 ) } )
proof
set p0 = |[0,0]|;
set p01 = |[0,1]|;
set p10 = |[1,0]|;
set p1 = |[1,1]|;
set L1 = { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } ;
set L2 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } ;
set L3 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } ;
set L4 = { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } ;
A1: |[0,1]| `2 = 1 by EUCLID:52;
A2: |[0,1]| `1 = 0 by EUCLID:52;
A3: LSeg (|[0,0]|,|[0,1]|) c= { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in LSeg (|[0,0]|,|[0,1]|) or a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } )
assume a in LSeg (|[0,0]|,|[0,1]|) ; ::_thesis: a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) }
then consider lambda being Real such that
A4: a = ((1 - lambda) * |[0,0]|) + (lambda * |[0,1]|) and
A5: 0 <= lambda and
A6: lambda <= 1 ;
set q = ((1 - lambda) * |[0,0]|) + (lambda * |[0,1]|);
A7: ((1 - lambda) * |[0,0]|) + (lambda * |[0,1]|) = (0. (TOP-REAL 2)) + (lambda * |[0,1]|) by EUCLID:28, EUCLID:54
.= lambda * |[0,1]| by EUCLID:27
.= |[(lambda * (|[0,1]| `1)),(lambda * (|[0,1]| `2))]| by EUCLID:57
.= |[0,lambda]| by A2, A1 ;
then A8: (((1 - lambda) * |[0,0]|) + (lambda * |[0,1]|)) `2 >= 0 by A5, EUCLID:52;
A9: (((1 - lambda) * |[0,0]|) + (lambda * |[0,1]|)) `1 = 0 by A7, EUCLID:52;
(((1 - lambda) * |[0,0]|) + (lambda * |[0,1]|)) `2 <= 1 by A6, A7, EUCLID:52;
hence a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } by A4, A9, A8; ::_thesis: verum
end;
{ p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } c= LSeg (|[0,0]|,|[0,1]|)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } or a in LSeg (|[0,0]|,|[0,1]|) )
assume a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } ; ::_thesis: a in LSeg (|[0,0]|,|[0,1]|)
then consider p being Point of (TOP-REAL 2) such that
A10: a = p and
A11: p `1 = 0 and
A12: p `2 <= 1 and
A13: p `2 >= 0 ;
set lambda = p `2 ;
((1 - (p `2)) * |[0,0]|) + ((p `2) * |[0,1]|) = (0. (TOP-REAL 2)) + ((p `2) * |[0,1]|) by EUCLID:28, EUCLID:54
.= (p `2) * |[0,1]| by EUCLID:27
.= |[((p `2) * (|[0,1]| `1)),((p `2) * (|[0,1]| `2))]| by EUCLID:57
.= p by A2, A1, A11, EUCLID:53 ;
hence a in LSeg (|[0,0]|,|[0,1]|) by A10, A12, A13; ::_thesis: verum
end;
hence { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } = LSeg (|[0,0]|,|[0,1]|) by A3, XBOOLE_0:def_10; ::_thesis: ( LSeg (|[0,1]|,|[1,1]|) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 1 ) } & LSeg (|[0,0]|,|[1,0]|) = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 <= 1 & q1 `1 >= 0 & q1 `2 = 0 ) } & LSeg (|[1,0]|,|[1,1]|) = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = 1 & q2 `2 <= 1 & q2 `2 >= 0 ) } )
A14: |[1,1]| `2 = 1 by EUCLID:52;
A15: |[1,1]| `1 = 1 by EUCLID:52;
A16: LSeg (|[0,1]|,|[1,1]|) c= { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in LSeg (|[0,1]|,|[1,1]|) or a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } )
assume a in LSeg (|[0,1]|,|[1,1]|) ; ::_thesis: a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) }
then consider lambda being Real such that
A17: a = ((1 - lambda) * |[0,1]|) + (lambda * |[1,1]|) and
A18: 0 <= lambda and
A19: lambda <= 1 ;
set q = ((1 - lambda) * |[0,1]|) + (lambda * |[1,1]|);
A20: ((1 - lambda) * |[0,1]|) + (lambda * |[1,1]|) = |[((1 - lambda) * 0),((1 - lambda) * (|[0,1]| `2))]| + (lambda * |[1,1]|) by A2, EUCLID:57
.= |[0,(1 - lambda)]| + |[lambda,(lambda * 1)]| by A1, A15, A14, EUCLID:57
.= |[(0 + lambda),((1 - lambda) + lambda)]| by EUCLID:56
.= |[lambda,1]| ;
then A21: (((1 - lambda) * |[0,1]|) + (lambda * |[1,1]|)) `1 >= 0 by A18, EUCLID:52;
A22: (((1 - lambda) * |[0,1]|) + (lambda * |[1,1]|)) `2 = 1 by A20, EUCLID:52;
(((1 - lambda) * |[0,1]|) + (lambda * |[1,1]|)) `1 <= 1 by A19, A20, EUCLID:52;
hence a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } by A17, A21, A22; ::_thesis: verum
end;
{ p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } c= LSeg (|[0,1]|,|[1,1]|)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } or a in LSeg (|[0,1]|,|[1,1]|) )
assume a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } ; ::_thesis: a in LSeg (|[0,1]|,|[1,1]|)
then consider p being Point of (TOP-REAL 2) such that
A23: a = p and
A24: p `1 <= 1 and
A25: p `1 >= 0 and
A26: p `2 = 1 ;
set lambda = p `1 ;
((1 - (p `1)) * |[0,1]|) + ((p `1) * |[1,1]|) = |[((1 - (p `1)) * 0),((1 - (p `1)) * (|[0,1]| `2))]| + ((p `1) * |[1,1]|) by A2, EUCLID:57
.= |[0,(1 - (p `1))]| + |[((p `1) * 1),(p `1)]| by A1, A15, A14, EUCLID:57
.= |[(0 + (p `1)),((1 - (p `1)) + (p `1))]| by EUCLID:56
.= p by A26, EUCLID:53 ;
hence a in LSeg (|[0,1]|,|[1,1]|) by A23, A24, A25; ::_thesis: verum
end;
hence { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } = LSeg (|[0,1]|,|[1,1]|) by A16, XBOOLE_0:def_10; ::_thesis: ( LSeg (|[0,0]|,|[1,0]|) = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 <= 1 & q1 `1 >= 0 & q1 `2 = 0 ) } & LSeg (|[1,0]|,|[1,1]|) = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = 1 & q2 `2 <= 1 & q2 `2 >= 0 ) } )
A27: |[1,0]| `2 = 0 by EUCLID:52;
A28: |[1,0]| `1 = 1 by EUCLID:52;
A29: LSeg (|[0,0]|,|[1,0]|) c= { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in LSeg (|[0,0]|,|[1,0]|) or a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } )
assume a in LSeg (|[0,0]|,|[1,0]|) ; ::_thesis: a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) }
then consider lambda being Real such that
A30: a = ((1 - lambda) * |[0,0]|) + (lambda * |[1,0]|) and
A31: 0 <= lambda and
A32: lambda <= 1 ;
set q = ((1 - lambda) * |[0,0]|) + (lambda * |[1,0]|);
A33: ((1 - lambda) * |[0,0]|) + (lambda * |[1,0]|) = (0. (TOP-REAL 2)) + (lambda * |[1,0]|) by EUCLID:28, EUCLID:54
.= lambda * |[1,0]| by EUCLID:27
.= |[(lambda * (|[1,0]| `1)),(lambda * (|[1,0]| `2))]| by EUCLID:57
.= |[lambda,0]| by A28, A27 ;
then A34: (((1 - lambda) * |[0,0]|) + (lambda * |[1,0]|)) `1 >= 0 by A31, EUCLID:52;
A35: (((1 - lambda) * |[0,0]|) + (lambda * |[1,0]|)) `2 = 0 by A33, EUCLID:52;
(((1 - lambda) * |[0,0]|) + (lambda * |[1,0]|)) `1 <= 1 by A32, A33, EUCLID:52;
hence a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } by A30, A34, A35; ::_thesis: verum
end;
A36: LSeg (|[1,0]|,|[1,1]|) c= { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in LSeg (|[1,0]|,|[1,1]|) or a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } )
assume a in LSeg (|[1,0]|,|[1,1]|) ; ::_thesis: a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) }
then consider lambda being Real such that
A37: a = ((1 - lambda) * |[1,0]|) + (lambda * |[1,1]|) and
A38: 0 <= lambda and
A39: lambda <= 1 ;
set q = ((1 - lambda) * |[1,0]|) + (lambda * |[1,1]|);
A40: ((1 - lambda) * |[1,0]|) + (lambda * |[1,1]|) = |[((1 - lambda) * 1),((1 - lambda) * (|[1,0]| `2))]| + (lambda * |[1,1]|) by A28, EUCLID:57
.= |[(1 - lambda),0]| + |[lambda,(lambda * 1)]| by A15, A14, A27, EUCLID:57
.= |[((1 - lambda) + lambda),(0 + lambda)]| by EUCLID:56
.= |[1,lambda]| ;
then A41: (((1 - lambda) * |[1,0]|) + (lambda * |[1,1]|)) `2 >= 0 by A38, EUCLID:52;
A42: (((1 - lambda) * |[1,0]|) + (lambda * |[1,1]|)) `1 = 1 by A40, EUCLID:52;
(((1 - lambda) * |[1,0]|) + (lambda * |[1,1]|)) `2 <= 1 by A39, A40, EUCLID:52;
hence a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } by A37, A42, A41; ::_thesis: verum
end;
{ p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } c= LSeg (|[0,0]|,|[1,0]|)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } or a in LSeg (|[0,0]|,|[1,0]|) )
assume a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } ; ::_thesis: a in LSeg (|[0,0]|,|[1,0]|)
then consider p being Point of (TOP-REAL 2) such that
A43: a = p and
A44: p `1 <= 1 and
A45: p `1 >= 0 and
A46: p `2 = 0 ;
set lambda = p `1 ;
((1 - (p `1)) * |[0,0]|) + ((p `1) * |[1,0]|) = (0. (TOP-REAL 2)) + ((p `1) * |[1,0]|) by EUCLID:28, EUCLID:54
.= (p `1) * |[1,0]| by EUCLID:27
.= |[((p `1) * (|[1,0]| `1)),((p `1) * (|[1,0]| `2))]| by EUCLID:57
.= p by A28, A27, A46, EUCLID:53 ;
hence a in LSeg (|[0,0]|,|[1,0]|) by A43, A44, A45; ::_thesis: verum
end;
hence { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } = LSeg (|[0,0]|,|[1,0]|) by A29, XBOOLE_0:def_10; ::_thesis: LSeg (|[1,0]|,|[1,1]|) = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = 1 & q2 `2 <= 1 & q2 `2 >= 0 ) }
{ p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } c= LSeg (|[1,0]|,|[1,1]|)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } or a in LSeg (|[1,0]|,|[1,1]|) )
assume a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } ; ::_thesis: a in LSeg (|[1,0]|,|[1,1]|)
then consider p being Point of (TOP-REAL 2) such that
A47: a = p and
A48: p `1 = 1 and
A49: p `2 <= 1 and
A50: p `2 >= 0 ;
set lambda = p `2 ;
((1 - (p `2)) * |[1,0]|) + ((p `2) * |[1,1]|) = |[((1 - (p `2)) * 1),((1 - (p `2)) * (|[1,0]| `2))]| + ((p `2) * |[1,1]|) by A28, EUCLID:57
.= |[(1 - (p `2)),0]| + |[((p `2) * 1),(p `2)]| by A15, A14, A27, EUCLID:57
.= |[((1 - (p `2)) + (p `2)),(0 + (p `2))]| by EUCLID:56
.= p by A48, EUCLID:53 ;
hence a in LSeg (|[1,0]|,|[1,1]|) by A47, A49, A50; ::_thesis: verum
end;
hence { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } = LSeg (|[1,0]|,|[1,1]|) by A36, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: TOPREAL1:14
R^2-unit_square = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) or ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) or ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) or ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) ) }
proof
defpred S1[ Point of (TOP-REAL 2)] means ( $1 `1 = 1 & $1 `2 <= 1 & $1 `2 >= 0 );
defpred S2[ Point of (TOP-REAL 2)] means ( $1 `1 <= 1 & $1 `1 >= 0 & $1 `2 = 0 );
defpred S3[ Point of (TOP-REAL 2)] means ( $1 `1 <= 1 & $1 `1 >= 0 & $1 `2 = 1 );
defpred S4[ Point of (TOP-REAL 2)] means ( $1 `1 = 0 & $1 `2 <= 1 & $1 `2 >= 0 );
defpred S5[ Point of (TOP-REAL 2)] means ( ( $1 `1 <= 1 & $1 `1 >= 0 & $1 `2 = 0 ) or ( $1 `1 = 1 & $1 `2 <= 1 & $1 `2 >= 0 ) );
defpred S6[ Point of (TOP-REAL 2)] means ( ( $1 `1 = 0 & $1 `2 <= 1 & $1 `2 >= 0 ) or ( $1 `1 <= 1 & $1 `1 >= 0 & $1 `2 = 1 ) );
set L1 = { p where p is Point of (TOP-REAL 2) : S4[p] } ;
set L2 = { p where p is Point of (TOP-REAL 2) : S3[p] } ;
set L3 = { p where p is Point of (TOP-REAL 2) : S2[p] } ;
set L4 = { p where p is Point of (TOP-REAL 2) : S1[p] } ;
A1: { p2 where p2 is Point of (TOP-REAL 2) : ( S6[p2] or S5[p2] ) } = { p where p is Point of (TOP-REAL 2) : S6[p] } \/ { q1 where q1 is Point of (TOP-REAL 2) : S5[q1] } from TOPREAL1:sch_1();
A2: { q1 where q1 is Point of (TOP-REAL 2) : ( S2[q1] or S1[q1] ) } = { p where p is Point of (TOP-REAL 2) : S2[p] } \/ { p where p is Point of (TOP-REAL 2) : S1[p] } from TOPREAL1:sch_1()
.= (LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)) by Th13 ;
{ p where p is Point of (TOP-REAL 2) : ( S4[p] or S3[p] ) } = { p where p is Point of (TOP-REAL 2) : S4[p] } \/ { p where p is Point of (TOP-REAL 2) : S3[p] } from TOPREAL1:sch_1()
.= (LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)) by Th13 ;
hence R^2-unit_square = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) or ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) or ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) or ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) ) } by A1, A2; ::_thesis: verum
end;
registration
cluster R^2-unit_square -> non empty ;
coherence
not R^2-unit_square is empty ;
end;
theorem :: TOPREAL1:15
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {|[0,1]|}
proof
for a being set holds
( a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) iff a = |[0,1]| )
proof
set p00 = |[0,0]|;
set p01 = |[0,1]|;
set p11 = |[1,1]|;
let a be set ; ::_thesis: ( a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) iff a = |[0,1]| )
thus ( a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) implies a = |[0,1]| ) ::_thesis: ( a = |[0,1]| implies a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) )
proof
assume A1: a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) ; ::_thesis: a = |[0,1]|
then a in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 1 ) } by Th13, XBOOLE_0:def_4;
then A2: ex p2 being Point of (TOP-REAL 2) st
( p2 = a & p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 1 ) ;
a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } by A1, Th13, XBOOLE_0:def_4;
then ex p being Point of (TOP-REAL 2) st
( p = a & p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) ;
hence a = |[0,1]| by A2, EUCLID:53; ::_thesis: verum
end;
assume A3: a = |[0,1]| ; ::_thesis: a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|))
then A4: a in LSeg (|[0,1]|,|[1,1]|) by RLTOPSP1:68;
a in LSeg (|[0,0]|,|[0,1]|) by A3, RLTOPSP1:68;
hence a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
hence (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {|[0,1]|} by TARSKI:def_1; ::_thesis: verum
end;
theorem :: TOPREAL1:16
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {|[1,0]|}
proof
for a being set holds
( a in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) iff a = |[1,0]| )
proof
set p00 = |[0,0]|;
set p10 = |[1,0]|;
set p11 = |[1,1]|;
let a be set ; ::_thesis: ( a in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) iff a = |[1,0]| )
thus ( a in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) implies a = |[1,0]| ) ::_thesis: ( a = |[1,0]| implies a in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) )
proof
assume A1: a in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) ; ::_thesis: a = |[1,0]|
then a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } by Th13, XBOOLE_0:def_4;
then A2: ex p being Point of (TOP-REAL 2) st
( p = a & p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) ;
a in LSeg (|[1,0]|,|[1,1]|) by A1, XBOOLE_0:def_4;
then ex p2 being Point of (TOP-REAL 2) st
( p2 = a & p2 `1 = 1 & p2 `2 <= 1 & p2 `2 >= 0 ) by Th13;
hence a = |[1,0]| by A2, EUCLID:53; ::_thesis: verum
end;
assume A3: a = |[1,0]| ; ::_thesis: a in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|))
then A4: a in LSeg (|[1,0]|,|[1,1]|) by RLTOPSP1:68;
a in LSeg (|[0,0]|,|[1,0]|) by A3, RLTOPSP1:68;
hence a in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
hence (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {|[1,0]|} by TARSKI:def_1; ::_thesis: verum
end;
theorem Th17: :: TOPREAL1:17
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {|[0,0]|}
proof
for a being set holds
( a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) iff a = |[0,0]| )
proof
let a be set ; ::_thesis: ( a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) iff a = |[0,0]| )
thus ( a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) implies a = |[0,0]| ) ::_thesis: ( a = |[0,0]| implies a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) )
proof
assume A1: a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) ; ::_thesis: a = |[0,0]|
then a in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 0 ) } by Th13, XBOOLE_0:def_4;
then A2: ex p2 being Point of (TOP-REAL 2) st
( p2 = a & p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 0 ) ;
a in LSeg (|[0,0]|,|[0,1]|) by A1, XBOOLE_0:def_4;
then ex p being Point of (TOP-REAL 2) st
( p = a & p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) by Th13;
hence a = |[0,0]| by A2, EUCLID:53; ::_thesis: verum
end;
assume A3: a = |[0,0]| ; ::_thesis: a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))
then A4: a in LSeg (|[0,0]|,|[1,0]|) by RLTOPSP1:68;
a in LSeg (|[0,0]|,|[0,1]|) by A3, RLTOPSP1:68;
hence a in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
hence (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {|[0,0]|} by TARSKI:def_1; ::_thesis: verum
end;
theorem Th18: :: TOPREAL1:18
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {|[1,1]|}
proof
for a being set holds
( a in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) iff a = |[1,1]| )
proof
let a be set ; ::_thesis: ( a in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) iff a = |[1,1]| )
thus ( a in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) implies a = |[1,1]| ) ::_thesis: ( a = |[1,1]| implies a in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) )
proof
assume A1: a in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) ; ::_thesis: a = |[1,1]|
then a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } by Th13, XBOOLE_0:def_4;
then A2: ex p being Point of (TOP-REAL 2) st
( p = a & p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) ;
a in LSeg (|[1,0]|,|[1,1]|) by A1, XBOOLE_0:def_4;
then ex p2 being Point of (TOP-REAL 2) st
( p2 = a & p2 `1 = 1 & p2 `2 <= 1 & p2 `2 >= 0 ) by Th13;
hence a = |[1,1]| by A2, EUCLID:53; ::_thesis: verum
end;
assume A3: a = |[1,1]| ; ::_thesis: a in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|))
then A4: a in LSeg (|[1,0]|,|[1,1]|) by RLTOPSP1:68;
a in LSeg (|[0,1]|,|[1,1]|) by A3, RLTOPSP1:68;
hence a in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
hence (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {|[1,1]|} by TARSKI:def_1; ::_thesis: verum
end;
theorem :: TOPREAL1:19
LSeg (|[0,0]|,|[1,0]|) misses LSeg (|[0,1]|,|[1,1]|)
proof
set x = the Element of (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|));
assume A1: (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then the Element of (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) in LSeg (|[0,1]|,|[1,1]|) by XBOOLE_0:def_4;
then A2: ex p being Point of (TOP-REAL 2) st
( p = the Element of (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) & p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) by Th13;
the Element of (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) in LSeg (|[0,0]|,|[1,0]|) by A1, XBOOLE_0:def_4;
then ex p2 being Point of (TOP-REAL 2) st
( p2 = the Element of (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) & p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 0 ) by Th13;
hence contradiction by A2; ::_thesis: verum
end;
theorem Th20: :: TOPREAL1:20
LSeg (|[0,0]|,|[0,1]|) misses LSeg (|[1,0]|,|[1,1]|)
proof
set x = the Element of (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|));
assume A1: (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then the Element of (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) in LSeg (|[0,0]|,|[0,1]|) by XBOOLE_0:def_4;
then A2: ex p being Point of (TOP-REAL 2) st
( p = the Element of (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) & p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) by Th13;
the Element of (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) in LSeg (|[1,0]|,|[1,1]|) by A1, XBOOLE_0:def_4;
then ex p2 being Point of (TOP-REAL 2) st
( p2 = the Element of (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) & p2 `1 = 1 & p2 `2 <= 1 & p2 `2 >= 0 ) by Th13;
hence contradiction by A2; ::_thesis: verum
end;
definition
let n be Nat;
let f be FinSequence of (TOP-REAL n);
let i be Nat;
func LSeg (f,i) -> Subset of (TOP-REAL n) equals :Def3: :: TOPREAL1:def 3
LSeg ((f /. i),(f /. (i + 1))) if ( 1 <= i & i + 1 <= len f )
otherwise {} ;
coherence
( ( 1 <= i & i + 1 <= len f implies LSeg ((f /. i),(f /. (i + 1))) is Subset of (TOP-REAL n) ) & ( ( not 1 <= i or not i + 1 <= len f ) implies {} is Subset of (TOP-REAL n) ) )
proof
thus ( 1 <= i & i + 1 <= len f implies LSeg ((f /. i),(f /. (i + 1))) is Subset of (TOP-REAL n) ) ; ::_thesis: ( ( not 1 <= i or not i + 1 <= len f ) implies {} is Subset of (TOP-REAL n) )
assume ( i < 1 or len f < i + 1 ) ; ::_thesis: {} is Subset of (TOP-REAL n)
{} (TOP-REAL n) is Subset of (TOP-REAL n) ;
hence {} is Subset of (TOP-REAL n) ; ::_thesis: verum
end;
correctness
consistency
for b1 being Subset of (TOP-REAL n) holds verum;
;
end;
:: deftheorem Def3 defines LSeg TOPREAL1:def_3_:_
for n being Nat
for f being FinSequence of (TOP-REAL n)
for i being Nat holds
( ( 1 <= i & i + 1 <= len f implies LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) ) & ( ( not 1 <= i or not i + 1 <= len f ) implies LSeg (f,i) = {} ) );
theorem Th21: :: TOPREAL1:21
for n, i being Nat
for f being FinSequence of (TOP-REAL n) st 1 <= i & i + 1 <= len f holds
( f /. i in LSeg (f,i) & f /. (i + 1) in LSeg (f,i) )
proof
let n, i be Nat; ::_thesis: for f being FinSequence of (TOP-REAL n) st 1 <= i & i + 1 <= len f holds
( f /. i in LSeg (f,i) & f /. (i + 1) in LSeg (f,i) )
let f be FinSequence of (TOP-REAL n); ::_thesis: ( 1 <= i & i + 1 <= len f implies ( f /. i in LSeg (f,i) & f /. (i + 1) in LSeg (f,i) ) )
assume that
A1: 1 <= i and
A2: i + 1 <= len f ; ::_thesis: ( f /. i in LSeg (f,i) & f /. (i + 1) in LSeg (f,i) )
LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A1, A2, Def3;
hence ( f /. i in LSeg (f,i) & f /. (i + 1) in LSeg (f,i) ) by RLTOPSP1:68; ::_thesis: verum
end;
definition
let n be Nat;
let f be FinSequence of (TOP-REAL n);
func L~ f -> Subset of (TOP-REAL n) equals :: TOPREAL1:def 4
union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;
coherence
union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } is Subset of (TOP-REAL n)
proof
set F = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;
{ (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } c= bool the carrier of (TOP-REAL n)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } or a in bool the carrier of (TOP-REAL n) )
assume a in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; ::_thesis: a in bool the carrier of (TOP-REAL n)
then ex i being Element of NAT st
( a = LSeg (f,i) & 1 <= i & i + 1 <= len f ) ;
hence a in bool the carrier of (TOP-REAL n) ; ::_thesis: verum
end;
then reconsider F = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } as Subset-Family of (TOP-REAL n) ;
union F is Subset of (TOP-REAL n) ;
hence union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } is Subset of (TOP-REAL n) ; ::_thesis: verum
end;
end;
:: deftheorem defines L~ TOPREAL1:def_4_:_
for n being Nat
for f being FinSequence of (TOP-REAL n) holds L~ f = union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;
theorem Th22: :: TOPREAL1:22
for n being Nat
for f being FinSequence of (TOP-REAL n) holds
( ( len f = 0 or len f = 1 ) iff L~ f = {} )
proof
let n be Nat; ::_thesis: for f being FinSequence of (TOP-REAL n) holds
( ( len f = 0 or len f = 1 ) iff L~ f = {} )
let f be FinSequence of (TOP-REAL n); ::_thesis: ( ( len f = 0 or len f = 1 ) iff L~ f = {} )
thus ( ( len f = 0 or len f = 1 ) implies L~ f = {} ) ::_thesis: ( not L~ f = {} or len f = 0 or len f = 1 )
proof
set L = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;
set x = the Element of { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;
assume A1: ( len f = 0 or len f = 1 ) ; ::_thesis: L~ f = {}
now__::_thesis:_L~_f_=_{}
percases ( len f = 0 or len f = 0 + 1 ) by A1;
supposeA2: len f = 0 ; ::_thesis: L~ f = {}
now__::_thesis:_not__{__(LSeg_(f,i))_where_i_is_Element_of_NAT_:_(_1_<=_i_&_i_+_1_<=_len_f_)__}__<>_{}
assume { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } <> {} ; ::_thesis: contradiction
then the Element of { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;
then ex i being Element of NAT st
( the Element of { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } = LSeg (f,i) & 1 <= i & i + 1 <= len f ) ;
hence contradiction by A2; ::_thesis: verum
end;
hence L~ f = {} by ZFMISC_1:2; ::_thesis: verum
end;
supposeA3: len f = 0 + 1 ; ::_thesis: L~ f = {}
now__::_thesis:_not__{__(LSeg_(f,i))_where_i_is_Element_of_NAT_:_(_1_<=_i_&_i_+_1_<=_len_f_)__}__<>_{}
assume { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } <> {} ; ::_thesis: contradiction
then the Element of { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;
then ex i being Element of NAT st
( the Element of { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } = LSeg (f,i) & 1 <= i & i + 1 <= len f ) ;
hence contradiction by A3, XREAL_1:6; ::_thesis: verum
end;
hence L~ f = {} by ZFMISC_1:2; ::_thesis: verum
end;
end;
end;
hence L~ f = {} ; ::_thesis: verum
end;
set L = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;
assume A4: L~ f = {} ; ::_thesis: ( len f = 0 or len f = 1 )
assume that
A5: len f <> 0 and
A6: len f <> 1 ; ::_thesis: contradiction
now__::_thesis:_not_len_f_<=_1
assume len f <= 1 ; ::_thesis: contradiction
then len f < 0 + 1 by A6, XXREAL_0:1;
hence contradiction by A5, NAT_1:13; ::_thesis: verum
end;
then A7: len f >= 1 + 1 by NAT_1:13;
then LSeg (f,1) in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;
then LSeg (f,1) = {} by A4, XBOOLE_1:3, ZFMISC_1:74;
hence contradiction by A7, Th21; ::_thesis: verum
end;
theorem Th23: :: TOPREAL1:23
for n being Nat
for f being FinSequence of (TOP-REAL n) st len f >= 2 holds
L~ f <> {}
proof
let n be Nat; ::_thesis: for f being FinSequence of (TOP-REAL n) st len f >= 2 holds
L~ f <> {}
let f be FinSequence of (TOP-REAL n); ::_thesis: ( len f >= 2 implies L~ f <> {} )
assume A1: len f >= 2 ; ::_thesis: L~ f <> {}
then not len f = 1 ;
hence L~ f <> {} by A1, Th22; ::_thesis: verum
end;
definition
let IT be FinSequence of (TOP-REAL 2);
attrIT is special means :: TOPREAL1:def 5
for i being Nat st 1 <= i & i + 1 <= len IT & not (IT /. i) `1 = (IT /. (i + 1)) `1 holds
(IT /. i) `2 = (IT /. (i + 1)) `2 ;
attrIT is unfolded means :Def6: :: TOPREAL1:def 6
for i being Nat st 1 <= i & i + 2 <= len IT holds
(LSeg (IT,i)) /\ (LSeg (IT,(i + 1))) = {(IT /. (i + 1))};
attrIT is s.n.c. means :Def7: :: TOPREAL1:def 7
for i, j being Nat st i + 1 < j holds
LSeg (IT,i) misses LSeg (IT,j);
end;
:: deftheorem defines special TOPREAL1:def_5_:_
for IT being FinSequence of (TOP-REAL 2) holds
( IT is special iff for i being Nat st 1 <= i & i + 1 <= len IT & not (IT /. i) `1 = (IT /. (i + 1)) `1 holds
(IT /. i) `2 = (IT /. (i + 1)) `2 );
:: deftheorem Def6 defines unfolded TOPREAL1:def_6_:_
for IT being FinSequence of (TOP-REAL 2) holds
( IT is unfolded iff for i being Nat st 1 <= i & i + 2 <= len IT holds
(LSeg (IT,i)) /\ (LSeg (IT,(i + 1))) = {(IT /. (i + 1))} );
:: deftheorem Def7 defines s.n.c. TOPREAL1:def_7_:_
for IT being FinSequence of (TOP-REAL 2) holds
( IT is s.n.c. iff for i, j being Nat st i + 1 < j holds
LSeg (IT,i) misses LSeg (IT,j) );
definition
let f be FinSequence of (TOP-REAL 2);
attrf is being_S-Seq means :Def8: :: TOPREAL1:def 8
( f is one-to-one & len f >= 2 & f is unfolded & f is s.n.c. & f is special );
end;
:: deftheorem Def8 defines being_S-Seq TOPREAL1:def_8_:_
for f being FinSequence of (TOP-REAL 2) holds
( f is being_S-Seq iff ( f is one-to-one & len f >= 2 & f is unfolded & f is s.n.c. & f is special ) );
theorem Th24: :: TOPREAL1:24
ex f1, f2 being FinSequence of (TOP-REAL 2) st
( f1 is being_S-Seq & f2 is being_S-Seq & R^2-unit_square = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {|[0,0]|,|[1,1]|} & f1 /. 1 = |[0,0]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0,0]| & f2 /. (len f2) = |[1,1]| )
proof
set p0 = |[0,0]|;
set p01 = |[0,1]|;
set p10 = |[1,0]|;
set p1 = |[1,1]|;
set L4 = { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } ;
set L3 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } ;
set L2 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } ;
set L1 = { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } ;
A1: |[1,1]| `1 = 1 by EUCLID:52;
reconsider f2 = <*|[0,0]|,|[1,0]|,|[1,1]|*> as FinSequence of (TOP-REAL 2) ;
reconsider f1 = <*|[0,0]|,|[0,1]|,|[1,1]|*> as FinSequence of (TOP-REAL 2) ;
A2: |[0,0]| `1 = 0 by EUCLID:52;
take f1 ; ::_thesis: ex f2 being FinSequence of (TOP-REAL 2) st
( f1 is being_S-Seq & f2 is being_S-Seq & R^2-unit_square = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {|[0,0]|,|[1,1]|} & f1 /. 1 = |[0,0]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0,0]| & f2 /. (len f2) = |[1,1]| )
take f2 ; ::_thesis: ( f1 is being_S-Seq & f2 is being_S-Seq & R^2-unit_square = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {|[0,0]|,|[1,1]|} & f1 /. 1 = |[0,0]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0,0]| & f2 /. (len f2) = |[1,1]| )
A3: f1 /. 2 = |[0,1]| by FINSEQ_4:18;
now__::_thesis:_not__{__p_where_p_is_Point_of_(TOP-REAL_2)_:_(_p_`1_<=_1_&_p_`1_>=_0_&_p_`2_=_1_)__}__meets__{__p_where_p_is_Point_of_(TOP-REAL_2)_:_(_p_`1_<=_1_&_p_`1_>=_0_&_p_`2_=_0_)__}_
assume { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } meets { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } ; ::_thesis: contradiction
then consider x being set such that
A4: x in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } and
A5: x in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } by XBOOLE_0:3;
A6: ex p2 being Point of (TOP-REAL 2) st
( p2 = x & p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 0 ) by A5;
ex p being Point of (TOP-REAL 2) st
( p = x & p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) by A4;
hence contradiction by A6; ::_thesis: verum
end;
then A7: { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } = {} by XBOOLE_0:def_7;
A8: |[1,0]| `2 = 0 by EUCLID:52;
A9: |[1,0]| `1 = 1 by EUCLID:52;
A10: len f2 = 1 + 2 by FINSEQ_1:45;
then A11: 1 + 1 <= len f2 ;
A12: f1 /. 3 = |[1,1]| by FINSEQ_4:18;
A13: f1 /. 1 = |[0,0]| by FINSEQ_4:18;
A14: { (LSeg (f1,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } c= {(LSeg (|[0,0]|,|[0,1]|)),(LSeg (|[0,1]|,|[1,1]|))}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (LSeg (f1,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } or a in {(LSeg (|[0,0]|,|[0,1]|)),(LSeg (|[0,1]|,|[1,1]|))} )
assume a in { (LSeg (f1,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } ; ::_thesis: a in {(LSeg (|[0,0]|,|[0,1]|)),(LSeg (|[0,1]|,|[1,1]|))}
then consider i being Element of NAT such that
A15: a = LSeg (f1,i) and
A16: 1 <= i and
A17: i + 1 <= len f1 ;
i + 1 <= 2 + 1 by A17, FINSEQ_1:45;
then i <= 1 + 1 by XREAL_1:6;
then ( i = 1 or i = 2 ) by A16, NAT_1:9;
then ( a = LSeg (|[0,0]|,|[0,1]|) or a = LSeg (|[0,1]|,|[1,1]|) ) by A13, A3, A12, A15, A17, Def3;
hence a in {(LSeg (|[0,0]|,|[0,1]|)),(LSeg (|[0,1]|,|[1,1]|))} by TARSKI:def_2; ::_thesis: verum
end;
A18: len f1 = 1 + 2 by FINSEQ_1:45;
then A19: 1 + 1 <= len f1 ;
1 + 1 in Seg (len f1) by A18, FINSEQ_1:1;
then LSeg (|[0,0]|,|[0,1]|) = LSeg (f1,1) by A18, A13, A3, Def3;
then A20: LSeg (|[0,0]|,|[0,1]|) in { (LSeg (f1,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } by A19;
A21: f2 /. 3 = |[1,1]| by FINSEQ_4:18;
A22: |[0,0]| `2 = 0 by EUCLID:52;
thus f1 is being_S-Seq ::_thesis: ( f2 is being_S-Seq & R^2-unit_square = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {|[0,0]|,|[1,1]|} & f1 /. 1 = |[0,0]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0,0]| & f2 /. (len f2) = |[1,1]| )
proof
A23: |[0,1]| <> |[1,1]| by A1, EUCLID:52;
|[0,0]| <> |[0,1]| by A22, EUCLID:52;
hence f1 is one-to-one by A1, A2, A23, FINSEQ_3:95; :: according to TOPREAL1:def_8 ::_thesis: ( len f1 >= 2 & f1 is unfolded & f1 is s.n.c. & f1 is special )
thus len f1 >= 2 by A18; ::_thesis: ( f1 is unfolded & f1 is s.n.c. & f1 is special )
thus f1 is unfolded ::_thesis: ( f1 is s.n.c. & f1 is special )
proof
A24: for x being set holds
( x in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) iff x = |[0,1]| )
proof
let x be set ; ::_thesis: ( x in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) iff x = |[0,1]| )
thus ( x in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) implies x = |[0,1]| ) ::_thesis: ( x = |[0,1]| implies x in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) )
proof
assume A25: x in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) ; ::_thesis: x = |[0,1]|
then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 1 ) } by Th13, XBOOLE_0:def_4;
then A26: ex p2 being Point of (TOP-REAL 2) st
( p2 = x & p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 1 ) ;
x in { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } by A25, Th13, XBOOLE_0:def_4;
then ex p being Point of (TOP-REAL 2) st
( p = x & p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) ;
hence x = |[0,1]| by A26, EUCLID:53; ::_thesis: verum
end;
assume A27: x = |[0,1]| ; ::_thesis: x in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|))
then A28: x in LSeg (|[0,1]|,|[1,1]|) by RLTOPSP1:68;
x in LSeg (|[0,0]|,|[0,1]|) by A27, RLTOPSP1:68;
hence x in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) by A28, XBOOLE_0:def_4; ::_thesis: verum
end;
let i be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( 1 <= i & i + 2 <= len f1 implies (LSeg (f1,i)) /\ (LSeg (f1,(i + 1))) = {(f1 /. (i + 1))} )
assume that
A29: 1 <= i and
A30: i + 2 <= len f1 ; ::_thesis: (LSeg (f1,i)) /\ (LSeg (f1,(i + 1))) = {(f1 /. (i + 1))}
i <= 1 by A18, A30, XREAL_1:6;
then A31: i = 1 by A29, XXREAL_0:1;
1 + 1 in Seg (len f1) by A18, FINSEQ_1:1;
then A32: LSeg (f1,1) = LSeg (|[0,0]|,|[0,1]|) by A18, A13, A3, Def3;
LSeg (f1,(1 + 1)) = LSeg (|[0,1]|,|[1,1]|) by A18, A3, A12, Def3;
hence (LSeg (f1,i)) /\ (LSeg (f1,(i + 1))) = {(f1 /. (i + 1))} by A3, A31, A32, A24, TARSKI:def_1; ::_thesis: verum
end;
thus f1 is s.n.c. ::_thesis: f1 is special
proof
let i be Nat; :: according to TOPREAL1:def_7 ::_thesis: for j being Nat st i + 1 < j holds
LSeg (f1,i) misses LSeg (f1,j)
let j be Nat; ::_thesis: ( i + 1 < j implies LSeg (f1,i) misses LSeg (f1,j) )
assume A33: i + 1 < j ; ::_thesis: LSeg (f1,i) misses LSeg (f1,j)
now__::_thesis:_(LSeg_(f1,i))_/\_(LSeg_(f1,j))_=_{}
percases ( 1 <= i or not 1 <= i or not i + 1 <= len f1 ) ;
suppose 1 <= i ; ::_thesis: (LSeg (f1,i)) /\ (LSeg (f1,j)) = {}
then A34: 1 + 1 <= i + 1 by XREAL_1:6;
now__::_thesis:_(_(_1_<=_j_&_j_+_1_<=_len_f1_&_contradiction_)_or_(_(_not_1_<=_j_or_not_j_+_1_<=_len_f1_)_&_(LSeg_(f1,i))_/\_(LSeg_(f1,j))_=_{}_)_)
percases ( ( 1 <= j & j + 1 <= len f1 ) or not 1 <= j or not j + 1 <= len f1 ) ;
case ( 1 <= j & j + 1 <= len f1 ) ; ::_thesis: contradiction
then j <= 2 by A18, XREAL_1:6;
hence contradiction by A33, A34, XXREAL_0:2; ::_thesis: verum
end;
case ( not 1 <= j or not j + 1 <= len f1 ) ; ::_thesis: (LSeg (f1,i)) /\ (LSeg (f1,j)) = {}
then LSeg (f1,j) = {} by Def3;
hence (LSeg (f1,i)) /\ (LSeg (f1,j)) = {} ; ::_thesis: verum
end;
end;
end;
hence (LSeg (f1,i)) /\ (LSeg (f1,j)) = {} ; ::_thesis: verum
end;
suppose ( not 1 <= i or not i + 1 <= len f1 ) ; ::_thesis: (LSeg (f1,i)) /\ (LSeg (f1,j)) = {}
then LSeg (f1,i) = {} by Def3;
hence (LSeg (f1,i)) /\ (LSeg (f1,j)) = {} ; ::_thesis: verum
end;
end;
end;
hence (LSeg (f1,i)) /\ (LSeg (f1,j)) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( 1 <= i & i + 1 <= len f1 & not (f1 /. i) `1 = (f1 /. (i + 1)) `1 implies (f1 /. i) `2 = (f1 /. (i + 1)) `2 )
assume that
A35: 1 <= i and
A36: i + 1 <= len f1 ; ::_thesis: ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 )
A37: i <= 1 + 1 by A18, A36, XREAL_1:6;
percases ( i = 1 or i = 2 ) by A35, A37, NAT_1:9;
supposeA38: i = 1 ; ::_thesis: ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 )
then (f1 /. i) `1 = |[0,0]| `1 by FINSEQ_4:18
.= 0 by EUCLID:52
.= (f1 /. (i + 1)) `1 by A3, A38, EUCLID:52 ;
hence ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 ) ; ::_thesis: verum
end;
supposeA39: i = 2 ; ::_thesis: ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 )
then (f1 /. i) `2 = |[0,1]| `2 by FINSEQ_4:18
.= 1 by EUCLID:52
.= (f1 /. (i + 1)) `2 by A12, A39, EUCLID:52 ;
hence ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 ) ; ::_thesis: verum
end;
end;
end;
A40: f2 /. 2 = |[1,0]| by FINSEQ_4:18;
A41: f2 /. 1 = |[0,0]| by FINSEQ_4:18;
A42: { (LSeg (f2,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } c= {(LSeg (|[0,0]|,|[1,0]|)),(LSeg (|[1,0]|,|[1,1]|))}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (LSeg (f2,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } or a in {(LSeg (|[0,0]|,|[1,0]|)),(LSeg (|[1,0]|,|[1,1]|))} )
assume a in { (LSeg (f2,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } ; ::_thesis: a in {(LSeg (|[0,0]|,|[1,0]|)),(LSeg (|[1,0]|,|[1,1]|))}
then consider i being Element of NAT such that
A43: a = LSeg (f2,i) and
A44: 1 <= i and
A45: i + 1 <= len f2 ;
i + 1 <= 2 + 1 by A45, FINSEQ_1:45;
then i <= 1 + 1 by XREAL_1:6;
then ( i = 1 or i = 2 ) by A44, NAT_1:9;
then ( a = LSeg (|[0,0]|,|[1,0]|) or a = LSeg (|[1,0]|,|[1,1]|) ) by A41, A40, A21, A43, A45, Def3;
hence a in {(LSeg (|[0,0]|,|[1,0]|)),(LSeg (|[1,0]|,|[1,1]|))} by TARSKI:def_2; ::_thesis: verum
end;
1 + 1 in Seg (len f2) by A10, FINSEQ_1:1;
then LSeg (|[0,0]|,|[1,0]|) = LSeg (f2,1) by A10, A41, A40, Def3;
then A46: LSeg (|[0,0]|,|[1,0]|) in { (LSeg (f2,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } by A11;
LSeg (|[1,0]|,|[1,1]|) = LSeg (f2,2) by A10, A40, A21, Def3;
then LSeg (|[1,0]|,|[1,1]|) in { (LSeg (f2,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } by A10;
then {(LSeg (|[0,0]|,|[1,0]|)),(LSeg (|[1,0]|,|[1,1]|))} c= { (LSeg (f2,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } by A46, ZFMISC_1:32;
then A47: L~ f2 = union {(LSeg (|[0,0]|,|[1,0]|)),(LSeg (|[1,0]|,|[1,1]|))} by A42, XBOOLE_0:def_10;
A48: |[1,1]| `2 = 1 by EUCLID:52;
thus f2 is being_S-Seq ::_thesis: ( R^2-unit_square = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {|[0,0]|,|[1,1]|} & f1 /. 1 = |[0,0]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0,0]| & f2 /. (len f2) = |[1,1]| )
proof
thus f2 is one-to-one by A1, A48, A9, A8, A2, FINSEQ_3:95; :: according to TOPREAL1:def_8 ::_thesis: ( len f2 >= 2 & f2 is unfolded & f2 is s.n.c. & f2 is special )
thus len f2 >= 2 by A10; ::_thesis: ( f2 is unfolded & f2 is s.n.c. & f2 is special )
thus f2 is unfolded ::_thesis: ( f2 is s.n.c. & f2 is special )
proof
A49: for x being set holds
( x in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) iff x = |[1,0]| )
proof
let x be set ; ::_thesis: ( x in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) iff x = |[1,0]| )
thus ( x in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) implies x = |[1,0]| ) ::_thesis: ( x = |[1,0]| implies x in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) )
proof
assume A50: x in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) ; ::_thesis: x = |[1,0]|
then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = 1 & p2 `2 <= 1 & p2 `2 >= 0 ) } by Th13, XBOOLE_0:def_4;
then A51: ex p2 being Point of (TOP-REAL 2) st
( p2 = x & p2 `1 = 1 & p2 `2 <= 1 & p2 `2 >= 0 ) ;
x in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } by A50, Th13, XBOOLE_0:def_4;
then ex p being Point of (TOP-REAL 2) st
( p = x & p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) ;
hence x = |[1,0]| by A51, EUCLID:53; ::_thesis: verum
end;
assume A52: x = |[1,0]| ; ::_thesis: x in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|))
then A53: x in LSeg (|[1,0]|,|[1,1]|) by RLTOPSP1:68;
x in LSeg (|[0,0]|,|[1,0]|) by A52, RLTOPSP1:68;
hence x in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) by A53, XBOOLE_0:def_4; ::_thesis: verum
end;
let i be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( 1 <= i & i + 2 <= len f2 implies (LSeg (f2,i)) /\ (LSeg (f2,(i + 1))) = {(f2 /. (i + 1))} )
assume that
A54: 1 <= i and
A55: i + 2 <= len f2 ; ::_thesis: (LSeg (f2,i)) /\ (LSeg (f2,(i + 1))) = {(f2 /. (i + 1))}
i <= 1 by A10, A55, XREAL_1:6;
then A56: i = 1 by A54, XXREAL_0:1;
1 + 1 in Seg (len f2) by A10, FINSEQ_1:1;
then A57: LSeg (f2,1) = LSeg (|[0,0]|,|[1,0]|) by A10, A41, A40, Def3;
LSeg (f2,(1 + 1)) = LSeg (|[1,0]|,|[1,1]|) by A10, A40, A21, Def3;
hence (LSeg (f2,i)) /\ (LSeg (f2,(i + 1))) = {(f2 /. (i + 1))} by A40, A56, A57, A49, TARSKI:def_1; ::_thesis: verum
end;
thus f2 is s.n.c. ::_thesis: f2 is special
proof
let i be Nat; :: according to TOPREAL1:def_7 ::_thesis: for j being Nat st i + 1 < j holds
LSeg (f2,i) misses LSeg (f2,j)
let j be Nat; ::_thesis: ( i + 1 < j implies LSeg (f2,i) misses LSeg (f2,j) )
assume A58: i + 1 < j ; ::_thesis: LSeg (f2,i) misses LSeg (f2,j)
percases ( 1 <= i or not 1 <= i or not i + 1 <= len f2 ) ;
suppose 1 <= i ; ::_thesis: LSeg (f2,i) misses LSeg (f2,j)
then A59: 1 + 1 <= i + 1 by XREAL_1:6;
now__::_thesis:_(_(_1_<=_j_&_j_+_1_<=_len_f2_&_contradiction_)_or_(_(_not_1_<=_j_or_not_j_+_1_<=_len_f2_)_&_(LSeg_(f2,i))_/\_(LSeg_(f2,j))_=_{}_)_)
percases ( ( 1 <= j & j + 1 <= len f2 ) or not 1 <= j or not j + 1 <= len f2 ) ;
case ( 1 <= j & j + 1 <= len f2 ) ; ::_thesis: contradiction
then j <= 2 by A10, XREAL_1:6;
hence contradiction by A58, A59, XXREAL_0:2; ::_thesis: verum
end;
case ( not 1 <= j or not j + 1 <= len f2 ) ; ::_thesis: (LSeg (f2,i)) /\ (LSeg (f2,j)) = {}
then LSeg (f2,j) = {} by Def3;
hence (LSeg (f2,i)) /\ (LSeg (f2,j)) = {} ; ::_thesis: verum
end;
end;
end;
hence (LSeg (f2,i)) /\ (LSeg (f2,j)) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
suppose ( not 1 <= i or not i + 1 <= len f2 ) ; ::_thesis: LSeg (f2,i) misses LSeg (f2,j)
then LSeg (f2,i) = {} by Def3;
hence (LSeg (f2,i)) /\ (LSeg (f2,j)) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
end;
end;
let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( 1 <= i & i + 1 <= len f2 & not (f2 /. i) `1 = (f2 /. (i + 1)) `1 implies (f2 /. i) `2 = (f2 /. (i + 1)) `2 )
assume that
A60: 1 <= i and
A61: i + 1 <= len f2 ; ::_thesis: ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 )
A62: i <= 1 + 1 by A10, A61, XREAL_1:6;
percases ( i = 1 or i = 2 ) by A60, A62, NAT_1:9;
supposeA63: i = 1 ; ::_thesis: ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 )
then (f2 /. i) `2 = |[0,0]| `2 by FINSEQ_4:18
.= 0 by EUCLID:52
.= (f2 /. (i + 1)) `2 by A40, A63, EUCLID:52 ;
hence ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 ) ; ::_thesis: verum
end;
supposeA64: i = 2 ; ::_thesis: ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 )
then (f2 /. i) `1 = |[1,0]| `1 by FINSEQ_4:18
.= 1 by EUCLID:52
.= (f2 /. (i + 1)) `1 by A21, A64, EUCLID:52 ;
hence ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 ) ; ::_thesis: verum
end;
end;
end;
A65: (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {} by Th20, XBOOLE_0:def_7;
LSeg (|[0,1]|,|[1,1]|) = LSeg (f1,2) by A18, A3, A12, Def3;
then LSeg (|[0,1]|,|[1,1]|) in { (LSeg (f1,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } by A18;
then {(LSeg (|[0,0]|,|[0,1]|)),(LSeg (|[0,1]|,|[1,1]|))} c= { (LSeg (f1,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } by A20, ZFMISC_1:32;
then A66: L~ f1 = union {(LSeg (|[0,0]|,|[0,1]|)),(LSeg (|[0,1]|,|[1,1]|))} by A14, XBOOLE_0:def_10;
then L~ f1 = (LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)) by ZFMISC_1:75;
hence R^2-unit_square = (L~ f1) \/ (L~ f2) by A47, ZFMISC_1:75; ::_thesis: ( (L~ f1) /\ (L~ f2) = {|[0,0]|,|[1,1]|} & f1 /. 1 = |[0,0]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0,0]| & f2 /. (len f2) = |[1,1]| )
L~ f2 = (LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)) by A47, ZFMISC_1:75;
hence (L~ f1) /\ (L~ f2) = ( { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } ) /\ ( { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } ) by A66, Th13, ZFMISC_1:75
.= (( { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } ) /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } ) \/ (( { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } ) /\ { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } ) by XBOOLE_1:23
.= (( { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } )) \/ (( { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } ) /\ { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } ) by XBOOLE_1:23
.= (( { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } )) \/ (( { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } )) by XBOOLE_1:23
.= {|[0,0]|,|[1,1]|} by A7, A65, Th13, Th17, Th18, ENUMSET1:1 ;
::_thesis: ( f1 /. 1 = |[0,0]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0,0]| & f2 /. (len f2) = |[1,1]| )
thus ( f1 /. 1 = |[0,0]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0,0]| & f2 /. (len f2) = |[1,1]| ) by A18, A10, FINSEQ_4:18; ::_thesis: verum
end;
theorem Th25: :: TOPREAL1:25
for h being FinSequence of (TOP-REAL 2) st h is being_S-Seq holds
L~ h is_an_arc_of h /. 1,h /. (len h)
proof
let h be FinSequence of (TOP-REAL 2); ::_thesis: ( h is being_S-Seq implies L~ h is_an_arc_of h /. 1,h /. (len h) )
set P = L~ h;
set p1 = h /. 1;
deffunc H1( Nat) -> Subset of (TOP-REAL 2) = L~ (h | ($1 + 2));
defpred S1[ Nat] means ( 1 <= $1 + 2 & $1 + 2 <= len h implies ex NE being non empty Subset of (TOP-REAL 2) st
( NE = H1($1) & ex f being Function of I[01],((TOP-REAL 2) | NE) st
( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. ($1 + 2) ) ) );
set p2 = h /. (1 + 1);
assume A1: h is being_S-Seq ; ::_thesis: L~ h is_an_arc_of h /. 1,h /. (len h)
then A2: len h >= 1 + 1 by Def8;
then 1 <= len h by XXREAL_0:2;
then A3: 1 in Seg (len h) by FINSEQ_1:1;
A4: h is one-to-one by A1, Def8;
A5: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A6: S1[n] ; ::_thesis: S1[n + 1]
set pn = h /. (n + 2);
set pn1 = h /. ((n + 2) + 1);
A7: (n + 1) + 1 <> (n + 2) + 1 ;
reconsider NE1 = H1(n) \/ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1)))) as non empty Subset of (TOP-REAL 2) ;
assume that
A8: 1 <= (n + 1) + 2 and
A9: (n + 1) + 2 <= len h ; ::_thesis: ex NE being non empty Subset of (TOP-REAL 2) st
( NE = H1(n + 1) & ex f being Function of I[01],((TOP-REAL 2) | NE) st
( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. ((n + 1) + 2) ) )
A10: (n + 2) + 1 in dom h by A8, A9, FINSEQ_3:25;
A11: (n + 1) + 1 <= (n + 2) + 1 by NAT_1:11;
then consider NE being non empty Subset of (TOP-REAL 2) such that
A12: NE = H1(n) and
A13: ex f being Function of I[01],((TOP-REAL 2) | NE) st
( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. (n + 2) ) by A6, A9, NAT_1:11, XXREAL_0:2;
A14: (n + 1) + 1 = n + (1 + 1) ;
now__::_thesis:_for_x_being_set_st_x_in_H1(n)_\/_(LSeg_(h,(n_+_2)))_holds_
x_in_H1(n_+_1)
let x be set ; ::_thesis: ( x in H1(n) \/ (LSeg (h,(n + 2))) implies x in H1(n + 1) )
assume A15: x in H1(n) \/ (LSeg (h,(n + 2))) ; ::_thesis: x in H1(n + 1)
now__::_thesis:_x_in_H1(n_+_1)
percases ( x in H1(n) or x in LSeg (h,(n + 2)) ) by A15, XBOOLE_0:def_3;
supposeA16: x in H1(n) ; ::_thesis: x in H1(n + 1)
A17: n + 1 <= n + (1 + 1) by XREAL_1:6;
consider X being set such that
A18: x in X and
A19: X in { (LSeg ((h | (n + 2)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | (n + 2)) ) } by A16, TARSKI:def_4;
consider i being Element of NAT such that
A20: X = LSeg ((h | (n + 2)),i) and
A21: 1 <= i and
A22: i + 1 <= len (h | (n + 2)) by A19;
i + 1 <= (n + 1) + 1 by A9, A11, A22, FINSEQ_1:59, XXREAL_0:2;
then i <= n + 1 by XREAL_1:6;
then A23: i <= n + 2 by A17, XXREAL_0:2;
len (h | (n + 2)) = n + 2 by A9, A11, FINSEQ_1:59, XXREAL_0:2;
then i in Seg (len (h | (n + 2))) by A21, A23, FINSEQ_1:1;
then A24: i in dom (h | (n + 2)) by FINSEQ_1:def_3;
set p19 = (h | (n + 2)) /. i;
set p29 = (h | (n + 2)) /. (i + 1);
A25: n + 2 <= (n + 2) + 1 by NAT_1:11;
then i <= (n + 1) + 2 by A23, XXREAL_0:2;
then i in Seg ((n + 1) + 2) by A21, FINSEQ_1:1;
then i in Seg (len (h | ((n + 1) + 2))) by A9, FINSEQ_1:59;
then i in dom (h | ((n + 1) + 2)) by FINSEQ_1:def_3;
then A26: (h | ((n + 1) + 2)) /. i = h /. i by FINSEQ_4:70
.= (h | (n + 2)) /. i by A24, FINSEQ_4:70 ;
i + 1 <= n + 2 by A9, A11, A22, FINSEQ_1:59, XXREAL_0:2;
then A27: i + 1 <= (n + 1) + 2 by A25, XXREAL_0:2;
A28: len (h | ((n + 1) + 2)) = (n + 1) + 2 by A9, FINSEQ_1:59;
A29: len (h | ((n + 1) + 2)) = n + (1 + 2) by A9, FINSEQ_1:59;
A30: n + 2 <= n + 3 by XREAL_1:6;
1 <= i + 1 by NAT_1:11;
then i + 1 in Seg (len (h | (n + 2))) by A22, FINSEQ_1:1;
then A31: i + 1 in dom (h | (n + 2)) by FINSEQ_1:def_3;
1 <= 1 + i by NAT_1:11;
then i + 1 in Seg ((n + 1) + 2) by A27, FINSEQ_1:1;
then i + 1 in Seg (len (h | ((n + 1) + 2))) by A9, FINSEQ_1:59;
then i + 1 in dom (h | ((n + 1) + 2)) by FINSEQ_1:def_3;
then A32: (h | ((n + 1) + 2)) /. (i + 1) = h /. (i + 1) by FINSEQ_4:70
.= (h | (n + 2)) /. (i + 1) by A31, FINSEQ_4:70 ;
i + 1 <= n + (1 + 1) by A9, A11, A22, FINSEQ_1:59, XXREAL_0:2;
then A33: i + 1 <= len (h | ((n + 1) + 2)) by A29, A30, XXREAL_0:2;
X = LSeg (((h | (n + 2)) /. i),((h | (n + 2)) /. (i + 1))) by A20, A21, A22, Def3
.= LSeg ((h | ((n + 1) + 2)),i) by A21, A27, A28, A26, A32, Def3 ;
then X in { (LSeg ((h | ((n + 1) + 2)),j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len (h | ((n + 1) + 2)) ) } by A21, A33;
hence x in H1(n + 1) by A18, TARSKI:def_4; ::_thesis: verum
end;
supposeA34: x in LSeg (h,(n + 2)) ; ::_thesis: x in H1(n + 1)
A35: 1 <= n + 2 by A14, NAT_1:11;
A36: len (h | ((n + 1) + 2)) = (n + 1) + 2 by A9, FINSEQ_1:59;
then (n + 2) + 1 in Seg (len (h | ((n + 1) + 2))) by A8, FINSEQ_1:1;
then A37: (n + 2) + 1 in dom (h | ((n + 1) + 2)) by FINSEQ_1:def_3;
then A38: (n + 2) + 1 <= len (h | ((n + 1) + 2)) by FINSEQ_3:25;
n + 2 <= (n + 2) + 1 by NAT_1:11;
then n + 2 in Seg (len (h | ((n + 1) + 2))) by A36, A35, FINSEQ_1:1;
then A39: n + 2 in dom (h | ((n + 1) + 2)) by FINSEQ_1:def_3;
then A40: 1 <= n + 2 by FINSEQ_3:25;
A41: h /. ((n + 2) + 1) = (h | ((n + 1) + 2)) /. ((n + 2) + 1) by A37, FINSEQ_4:70;
A42: h /. (n + 2) = (h | ((n + 1) + 2)) /. (n + 2) by A39, FINSEQ_4:70;
LSeg (h,(n + 2)) = LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))) by A9, A35, Def3
.= LSeg ((h | ((n + 1) + 2)),(n + 2)) by A36, A35, A42, A41, Def3 ;
then LSeg (h,(n + 2)) in { (LSeg ((h | ((n + 1) + 2)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | ((n + 1) + 2)) ) } by A40, A38;
hence x in H1(n + 1) by A34, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence x in H1(n + 1) ; ::_thesis: verum
end;
then A43: H1(n) \/ (LSeg (h,(n + 2))) c= H1(n + 1) by TARSKI:def_3;
take NE1 ; ::_thesis: ( NE1 = H1(n + 1) & ex f being Function of I[01],((TOP-REAL 2) | NE1) st
( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. ((n + 1) + 2) ) )
A44: 1 <= (n + 1) + 1 by NAT_1:11;
now__::_thesis:_for_x_being_set_st_x_in_H1(n_+_1)_holds_
x_in_H1(n)_\/_(LSeg_(h,(n_+_2)))
let x be set ; ::_thesis: ( x in H1(n + 1) implies x in H1(n) \/ (LSeg (h,(n + 2))) )
A45: n + (1 + 1) = (n + 1) + 1 ;
A46: (len (h | ((n + 1) + 2))) - 1 = ((n + 1) + 2) - 1 by A9, FINSEQ_1:59
.= n + (1 + 1) ;
assume x in H1(n + 1) ; ::_thesis: x in H1(n) \/ (LSeg (h,(n + 2)))
then consider X being set such that
A47: x in X and
A48: X in { (LSeg ((h | ((n + 1) + 2)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | ((n + 1) + 2)) ) } by TARSKI:def_4;
consider i being Element of NAT such that
A49: X = LSeg ((h | ((n + 1) + 2)),i) and
A50: 1 <= i and
A51: i + 1 <= len (h | ((n + 1) + 2)) by A48;
(i + 1) - 1 = i ;
then A52: i <= (len (h | ((n + 1) + 2))) - 1 by A51, XREAL_1:9;
now__::_thesis:_x_in_H1(n)_\/_(LSeg_(h,(n_+_2)))
percases ( i = n + 2 or i <= n + 1 ) by A52, A46, A45, NAT_1:8;
supposeA53: i = n + 2 ; ::_thesis: x in H1(n) \/ (LSeg (h,(n + 2)))
A54: len (h | ((n + 1) + 2)) = (n + 1) + 2 by A9, FINSEQ_1:59;
1 <= (n + 2) + 1 by NAT_1:11;
then (n + 2) + 1 in Seg (len (h | ((n + 1) + 2))) by A54, FINSEQ_1:1;
then (n + 2) + 1 in dom (h | ((n + 1) + 2)) by FINSEQ_1:def_3;
then A55: (h | ((n + 1) + 2)) /. ((n + 2) + 1) = h /. (n + (2 + 1)) by FINSEQ_4:70;
A56: 1 <= n + 2 by A14, NAT_1:11;
(n + 1) + 2 = (n + 2) + 1 ;
then n + 2 <= (n + 1) + 2 by NAT_1:11;
then n + 2 in Seg (len (h | ((n + 1) + 2))) by A54, A56, FINSEQ_1:1;
then n + 2 in dom (h | ((n + 1) + 2)) by FINSEQ_1:def_3;
then (h | ((n + 1) + 2)) /. (n + 2) = h /. (n + 2) by FINSEQ_4:70;
then LSeg ((h | ((n + 1) + 2)),(n + 2)) = LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))) by A54, A56, A55, Def3
.= LSeg (h,(n + 2)) by A9, A44, Def3 ;
hence x in H1(n) \/ (LSeg (h,(n + 2))) by A47, A49, A53, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA57: i <= n + 1 ; ::_thesis: x in H1(n) \/ (LSeg (h,(n + 2)))
then i + 1 <= (n + 1) + 1 by XREAL_1:6;
then i + 1 <= len (h | (n + 2)) by A9, A11, FINSEQ_1:59, XXREAL_0:2;
then A58: LSeg ((h | (n + 2)),i) in { (LSeg ((h | (n + 2)),j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len (h | (n + 2)) ) } by A50;
set p19 = (h | (n + 2)) /. i;
set p29 = (h | (n + 2)) /. (i + 1);
A59: 1 <= 1 + i by NAT_1:11;
A60: len (h | (n + 2)) = n + (1 + 1) by A9, A11, FINSEQ_1:59, XXREAL_0:2;
n + 1 <= (n + 1) + 1 by NAT_1:11;
then A61: i <= n + 2 by A57, XXREAL_0:2;
then i in Seg (len (h | (n + 2))) by A50, A60, FINSEQ_1:1;
then A62: i in dom (h | (n + 2)) by FINSEQ_1:def_3;
A63: i + 1 <= (n + 1) + 1 by A57, XREAL_1:7;
then i + 1 in Seg (len (h | (n + 2))) by A60, A59, FINSEQ_1:1;
then A64: i + 1 in dom (h | (n + 2)) by FINSEQ_1:def_3;
n + 2 <= (n + 2) + 1 by NAT_1:11;
then i <= (n + 1) + 2 by A61, XXREAL_0:2;
then i in Seg ((n + 1) + 2) by A50, FINSEQ_1:1;
then i in Seg (len (h | ((n + 1) + 2))) by A9, FINSEQ_1:59;
then i in dom (h | ((n + 1) + 2)) by FINSEQ_1:def_3;
then A65: (h | ((n + 1) + 2)) /. i = h /. i by FINSEQ_4:70
.= (h | (n + 2)) /. i by A62, FINSEQ_4:70 ;
i + 1 <= (n + 1) + 2 by A57, XREAL_1:7;
then i + 1 in Seg ((n + 1) + 2) by A59, FINSEQ_1:1;
then i + 1 in Seg (len (h | ((n + 1) + 2))) by A9, FINSEQ_1:59;
then i + 1 in dom (h | ((n + 1) + 2)) by FINSEQ_1:def_3;
then A66: (h | ((n + 1) + 2)) /. (i + 1) = h /. (i + 1) by FINSEQ_4:70
.= (h | (n + 2)) /. (i + 1) by A64, FINSEQ_4:70 ;
LSeg ((h | (n + 2)),i) = LSeg (((h | (n + 2)) /. i),((h | (n + 2)) /. (i + 1))) by A50, A60, A63, Def3
.= LSeg ((h | ((n + 1) + 2)),i) by A50, A51, A65, A66, Def3 ;
then x in union { (LSeg ((h | (n + 2)),j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len (h | (n + 2)) ) } by A47, A49, A58, TARSKI:def_4;
hence x in H1(n) \/ (LSeg (h,(n + 2))) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence x in H1(n) \/ (LSeg (h,(n + 2))) ; ::_thesis: verum
end;
then H1(n + 1) c= H1(n) \/ (LSeg (h,(n + 2))) by TARSKI:def_3;
then H1(n + 1) = H1(n) \/ (LSeg (h,(n + 2))) by A43, XBOOLE_0:def_10;
hence NE1 = H1(n + 1) by A9, A44, Def3; ::_thesis: ex f being Function of I[01],((TOP-REAL 2) | NE1) st
( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. ((n + 1) + 2) )
A67: (n + 1) + 1 <= len h by A9, A11, XXREAL_0:2;
then (n + 1) + 1 in dom h by A44, FINSEQ_3:25;
then LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))) is_an_arc_of h /. (n + 2),h /. ((n + 2) + 1) by A4, A7, A10, Th9, PARTFUN2:10;
then consider f1 being Function of I[01],((TOP-REAL 2) | (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))))) such that
A68: f1 is being_homeomorphism and
A69: f1 . 0 = h /. (n + 2) and
A70: f1 . 1 = h /. ((n + 2) + 1) by Def1;
consider f being Function of I[01],((TOP-REAL 2) | NE) such that
f is being_homeomorphism and
A71: f . 0 = h /. 1 and
f . 1 = h /. (n + 2) by A13;
for x being set holds
( x in H1(n) /\ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1)))) iff x = h /. (n + 2) )
proof
let x be set ; ::_thesis: ( x in H1(n) /\ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1)))) iff x = h /. (n + 2) )
A72: 1 <= n + 1 by NAT_1:11;
thus ( x in H1(n) /\ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1)))) implies x = h /. (n + 2) ) ::_thesis: ( x = h /. (n + 2) implies x in H1(n) /\ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1)))) )
proof
A73: 1 <= n + 1 by NAT_1:11;
h is unfolded by A1, Def8;
then A74: (LSeg (h,(n + 1))) /\ (LSeg (h,((n + 1) + 1))) = {(h /. ((n + 1) + 1))} by A9, A73, Def6;
A75: (n + 1) + 1 <= len h by A9, A11, XXREAL_0:2;
assume A76: x in H1(n) /\ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1)))) ; ::_thesis: x = h /. (n + 2)
then A77: x in LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))) by XBOOLE_0:def_4;
A78: LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))) = LSeg (h,((n + 1) + 1)) by A9, A44, Def3;
set p19 = h /. (n + 1);
set p29 = h /. ((n + 1) + 1);
A79: 1 <= 1 + n by NAT_1:11;
x in H1(n) by A76, XBOOLE_0:def_4;
then consider X being set such that
A80: x in X and
A81: X in { (LSeg ((h | (n + 2)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | (n + 2)) ) } by TARSKI:def_4;
consider i being Element of NAT such that
A82: X = LSeg ((h | (n + 2)),i) and
A83: 1 <= i and
A84: i + 1 <= len (h | (n + 2)) by A81;
A85: len (h | (n + 2)) = n + (1 + 1) by A9, A11, FINSEQ_1:59, XXREAL_0:2;
n + 1 <= (n + 1) + 1 by NAT_1:11;
then n + 1 in Seg (len (h | (n + 2))) by A85, A79, FINSEQ_1:1;
then n + 1 in dom (h | (n + 2)) by FINSEQ_1:def_3;
then A86: (h | (n + 2)) /. (n + 1) = h /. (n + 1) by FINSEQ_4:70;
1 <= 1 + (n + 1) by NAT_1:11;
then (n + 1) + 1 in Seg (len (h | (n + 2))) by A85, FINSEQ_1:1;
then (n + 1) + 1 in dom (h | (n + 2)) by FINSEQ_1:def_3;
then A87: (h | (n + 2)) /. ((n + 1) + 1) = h /. ((n + 1) + 1) by FINSEQ_4:70;
A88: len (h | (n + 2)) = (n + 1) + 1 by A9, A11, FINSEQ_1:59, XXREAL_0:2;
then A89: i <= n + 1 by A84, XREAL_1:6;
then 1 <= n + 1 by A83, XXREAL_0:2;
then A90: LSeg (h,(n + 1)) = LSeg ((h /. (n + 1)),(h /. ((n + 1) + 1))) by A75, Def3
.= LSeg ((h | (n + 2)),(n + 1)) by A85, A79, A86, A87, Def3 ;
A91: h is s.n.c. by A1, Def8;
now__::_thesis:_not_i_<_n_+_1
set p19 = h /. i;
set p29 = h /. (i + 1);
assume A92: i < n + 1 ; ::_thesis: contradiction
then A93: i + 1 < (n + 1) + 1 by XREAL_1:6;
n + 1 <= (n + 1) + 1 by NAT_1:11;
then i <= n + 2 by A92, XXREAL_0:2;
then i in Seg (len (h | (n + 2))) by A83, A85, FINSEQ_1:1;
then i in dom (h | (n + 2)) by FINSEQ_1:def_3;
then A94: (h | (n + 2)) /. i = h /. i by FINSEQ_4:70;
A95: LSeg (h,(n + 2)) = LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))) by A9, A44, Def3;
1 <= 1 + i by NAT_1:11;
then i + 1 in Seg (len (h | (n + 2))) by A84, FINSEQ_1:1;
then i + 1 in dom (h | (n + 2)) by FINSEQ_1:def_3;
then A96: (h | (n + 2)) /. (i + 1) = h /. (i + 1) by FINSEQ_4:70;
i + 1 <= len h by A67, A84, A88, XXREAL_0:2;
then LSeg (h,i) = LSeg ((h /. i),(h /. (i + 1))) by A83, Def3
.= LSeg ((h | (n + 2)),i) by A83, A84, A94, A96, Def3 ;
then LSeg ((h | (n + 2)),i) misses LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))) by A91, A93, A95, Def7;
hence contradiction by A77, A80, A82, XBOOLE_0:3; ::_thesis: verum
end;
then i = n + 1 by A89, XXREAL_0:1;
then x in (LSeg (h,(n + 1))) /\ (LSeg (h,((n + 1) + 1))) by A77, A80, A82, A90, A78, XBOOLE_0:def_4;
hence x = h /. (n + 2) by A74, TARSKI:def_1; ::_thesis: verum
end;
assume A97: x = h /. (n + 2) ; ::_thesis: x in H1(n) /\ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))))
A98: 1 <= n + 1 by NAT_1:11;
(n + 1) + 1 <= len (h | (n + 2)) by A9, A11, FINSEQ_1:59, XXREAL_0:2;
then A99: LSeg ((h | (n + 2)),(n + 1)) in { (LSeg ((h | (n + 2)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | (n + 2)) ) } by A98;
A100: n + 2 in Seg (n + 2) by A44, FINSEQ_1:1;
A101: len (h | (n + 2)) = n + 2 by A9, A11, FINSEQ_1:59, XXREAL_0:2;
then dom (h | (n + 2)) = Seg (n + 2) by FINSEQ_1:def_3;
then x = (h | (n + 2)) /. ((n + 1) + 1) by A97, A100, FINSEQ_4:70;
then x in LSeg ((h | (n + 2)),(n + 1)) by A101, A72, Th21;
then A102: x in union { (LSeg ((h | (n + 2)),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | (n + 2)) ) } by A99, TARSKI:def_4;
x in LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1))) by A97, RLTOPSP1:68;
hence x in H1(n) /\ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1)))) by A102, XBOOLE_0:def_4; ::_thesis: verum
end;
then H1(n) /\ (LSeg ((h /. (n + 2)),(h /. ((n + 2) + 1)))) = {(h /. (n + 2))} by TARSKI:def_1;
then consider hh being Function of I[01],((TOP-REAL 2) | NE1) such that
A103: hh is being_homeomorphism and
A104: hh . 0 = f . 0 and
A105: hh . 1 = f1 . 1 by A12, A13, A71, A68, A69, TOPMETR2:3;
take hh ; ::_thesis: ( hh is being_homeomorphism & hh . 0 = h /. 1 & hh . 1 = h /. ((n + 1) + 2) )
thus ( hh is being_homeomorphism & hh . 0 = h /. 1 & hh . 1 = h /. ((n + 1) + 2) ) by A71, A70, A103, A104, A105; ::_thesis: verum
end;
h | 2 = h | (Seg 2) by FINSEQ_1:def_15;
then A106: dom (h | 2) = (dom h) /\ (Seg 2) by RELAT_1:61
.= (Seg (len h)) /\ (Seg 2) by FINSEQ_1:def_3
.= Seg 2 by A2, FINSEQ_1:7 ;
then A107: len (h | 2) = 1 + 1 by FINSEQ_1:def_3;
then A108: 2 in Seg (len (h | 2)) by FINSEQ_1:1;
A109: 1 in Seg (len (h | 2)) by A107, FINSEQ_1:1;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in__{__(LSeg_((h_|_2),i))_where_i_is_Element_of_NAT_:_(_1_<=_i_&_i_+_1_<=_len_(h_|_2)_)__}__implies_x_=_LSeg_(h,1)_)_&_(_x_=_LSeg_(h,1)_implies_x_in__{__(LSeg_((h_|_2),i))_where_i_is_Element_of_NAT_:_(_1_<=_i_&_i_+_1_<=_len_(h_|_2)_)__}__)_)
let x be set ; ::_thesis: ( ( x in { (LSeg ((h | 2),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } implies x = LSeg (h,1) ) & ( x = LSeg (h,1) implies x in { (LSeg ((h | 2),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } ) )
A110: h /. (1 + 1) = (h | 2) /. 2 by A106, A107, A108, FINSEQ_4:70;
thus ( x in { (LSeg ((h | 2),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } implies x = LSeg (h,1) ) ::_thesis: ( x = LSeg (h,1) implies x in { (LSeg ((h | 2),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } )
proof
assume x in { (LSeg ((h | 2),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } ; ::_thesis: x = LSeg (h,1)
then consider i being Element of NAT such that
A111: x = LSeg ((h | 2),i) and
A112: 1 <= i and
A113: i + 1 <= len (h | 2) ;
i + 1 <= 1 + 1 by A106, A113, FINSEQ_1:def_3;
then i <= 1 by XREAL_1:6;
then A114: 1 = i by A112, XXREAL_0:1;
A115: (h | 2) /. (1 + 1) = h /. (1 + 1) by A106, A107, A108, FINSEQ_4:70;
(h | 2) /. 1 = h /. 1 by A106, A107, A109, FINSEQ_4:70;
hence x = LSeg ((h /. 1),(h /. (1 + 1))) by A107, A111, A114, A115, Def3
.= LSeg (h,1) by A2, Def3 ;
::_thesis: verum
end;
assume x = LSeg (h,1) ; ::_thesis: x in { (LSeg ((h | 2),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) }
then A116: x = LSeg ((h /. 1),(h /. (1 + 1))) by A2, Def3;
h /. 1 = (h | 2) /. 1 by A106, A107, A109, FINSEQ_4:70;
then x = LSeg ((h | 2),1) by A107, A116, A110, Def3;
hence x in { (LSeg ((h | 2),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } by A107; ::_thesis: verum
end;
then { (LSeg ((h | 2),i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len (h | 2) ) } = {(LSeg (h,1))} by TARSKI:def_1;
then A117: H1( 0 ) = LSeg (h,1) by ZFMISC_1:25
.= LSeg ((h /. 1),(h /. (1 + 1))) by A2, Def3 ;
A118: 1 + 1 in Seg (len h) by A2, FINSEQ_1:1;
( 1 <= 0 + 2 & 0 + 2 <= len h implies ex f being Function of I[01],((TOP-REAL 2) | (LSeg ((h /. 1),(h /. (1 + 1))))) st
( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. (0 + 2) ) )
proof
assume that
1 <= 0 + 2 and
0 + 2 <= len h ; ::_thesis: ex f being Function of I[01],((TOP-REAL 2) | (LSeg ((h /. 1),(h /. (1 + 1))))) st
( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. (0 + 2) )
A119: 2 in dom h by A118, FINSEQ_1:def_3;
1 in dom h by A3, FINSEQ_1:def_3;
then LSeg ((h /. 1),(h /. (1 + 1))) is_an_arc_of h /. 1,h /. (1 + 1) by A4, A119, Th9, PARTFUN2:10;
hence ex f being Function of I[01],((TOP-REAL 2) | (LSeg ((h /. 1),(h /. (1 + 1))))) st
( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. (0 + 2) ) by Def1; ::_thesis: verum
end;
then A120: S1[ 0 ] by A117;
A121: for n being Nat holds S1[n] from NAT_1:sch_2(A120, A5);
(len h) - 2 in NAT by A2, INT_1:5;
then reconsider h1 = (len h) - 2 as Nat ;
1 <= h1 + 2 by NAT_1:12;
then consider NE being non empty Subset of (TOP-REAL 2) such that
A122: NE = H1(h1) and
A123: ex f being Function of I[01],((TOP-REAL 2) | NE) st
( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. (h1 + 2) ) by A121;
consider f being Function of I[01],((TOP-REAL 2) | NE) such that
A124: f is being_homeomorphism and
A125: f . 0 = h /. 1 and
A126: f . 1 = h /. (h1 + 2) by A123;
A127: h | (len h) = h | (Seg (len h)) by FINSEQ_1:def_15
.= h | (dom h) by FINSEQ_1:def_3
.= h by RELAT_1:68 ;
then reconsider f = f as Function of I[01],((TOP-REAL 2) | (L~ h)) by A122;
take f ; :: according to TOPREAL1:def_1 ::_thesis: ( f is being_homeomorphism & f . 0 = h /. 1 & f . 1 = h /. (len h) )
thus f is being_homeomorphism by A122, A124, A127; ::_thesis: ( f . 0 = h /. 1 & f . 1 = h /. (len h) )
thus ( f . 0 = h /. 1 & f . 1 = h /. (len h) ) by A125, A126; ::_thesis: verum
end;
definition
let P be Subset of (TOP-REAL 2);
attrP is being_S-P_arc means :Def9: :: TOPREAL1:def 9
ex f being FinSequence of (TOP-REAL 2) st
( f is being_S-Seq & P = L~ f );
end;
:: deftheorem Def9 defines being_S-P_arc TOPREAL1:def_9_:_
for P being Subset of (TOP-REAL 2) holds
( P is being_S-P_arc iff ex f being FinSequence of (TOP-REAL 2) st
( f is being_S-Seq & P = L~ f ) );
theorem Th26: :: TOPREAL1:26
for P1 being Subset of (TOP-REAL 2) st P1 is being_S-P_arc holds
P1 <> {}
proof
let P1 be Subset of (TOP-REAL 2); ::_thesis: ( P1 is being_S-P_arc implies P1 <> {} )
assume P1 is being_S-P_arc ; ::_thesis: P1 <> {}
then consider f being FinSequence of (TOP-REAL 2) such that
A1: f is being_S-Seq and
A2: P1 = L~ f by Def9;
len f >= 2 by A1, Def8;
hence P1 <> {} by A2, Th23; ::_thesis: verum
end;
registration
cluster being_S-P_arc -> non empty for Element of K10( the carrier of (TOP-REAL 2));
coherence
for b1 being Subset of (TOP-REAL 2) st b1 is being_S-P_arc holds
not b1 is empty by Th26;
end;
theorem :: TOPREAL1:27
ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is being_S-P_arc & P2 is being_S-P_arc & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {|[0,0]|,|[1,1]|} )
proof
consider f1, f2 being FinSequence of (TOP-REAL 2) such that
A1: f1 is being_S-Seq and
A2: f2 is being_S-Seq and
A3: R^2-unit_square = (L~ f1) \/ (L~ f2) and
A4: (L~ f1) /\ (L~ f2) = {|[0,0]|,|[1,1]|} and
f1 /. 1 = |[0,0]| and
f1 /. (len f1) = |[1,1]| and
f2 /. 1 = |[0,0]| and
f2 /. (len f2) = |[1,1]| by Th24;
reconsider P1 = L~ f1, P2 = L~ f2 as non empty Subset of (TOP-REAL 2) by A4;
take P1 ; ::_thesis: ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is being_S-P_arc & P2 is being_S-P_arc & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {|[0,0]|,|[1,1]|} )
take P2 ; ::_thesis: ( P1 is being_S-P_arc & P2 is being_S-P_arc & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {|[0,0]|,|[1,1]|} )
thus ( P1 is being_S-P_arc & P2 is being_S-P_arc & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {|[0,0]|,|[1,1]|} ) by A1, A2, A3, A4, Def9; ::_thesis: verum
end;
theorem Th28: :: TOPREAL1:28
for P being Subset of (TOP-REAL 2) st P is being_S-P_arc holds
ex p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2
proof
let P be Subset of (TOP-REAL 2); ::_thesis: ( P is being_S-P_arc implies ex p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 )
assume P is being_S-P_arc ; ::_thesis: ex p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2
then consider h being FinSequence of (TOP-REAL 2) such that
A1: h is being_S-Seq and
A2: P = L~ h by Def9;
take h /. 1 ; ::_thesis: ex p2 being Point of (TOP-REAL 2) st P is_an_arc_of h /. 1,p2
take h /. (len h) ; ::_thesis: P is_an_arc_of h /. 1,h /. (len h)
thus P is_an_arc_of h /. 1,h /. (len h) by A1, A2, Th25; ::_thesis: verum
end;
theorem :: TOPREAL1:29
for P being Subset of (TOP-REAL 2) st P is being_S-P_arc holds
ex f being Function of I[01],((TOP-REAL 2) | P) st f is being_homeomorphism
proof
let P be Subset of (TOP-REAL 2); ::_thesis: ( P is being_S-P_arc implies ex f being Function of I[01],((TOP-REAL 2) | P) st f is being_homeomorphism )
assume P is being_S-P_arc ; ::_thesis: ex f being Function of I[01],((TOP-REAL 2) | P) st f is being_homeomorphism
then consider p1, p2 being Point of (TOP-REAL 2) such that
A1: P is_an_arc_of p1,p2 by Th28;
ex f being Function of I[01],((TOP-REAL 2) | P) st
( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) by A1, Def1;
hence ex f being Function of I[01],((TOP-REAL 2) | P) st f is being_homeomorphism ; ::_thesis: verum
end;
scheme :: TOPREAL1:sch 2
TRSubsetEx{ F1() -> Nat, P1[ set ] } :
ex A being Subset of (TOP-REAL F1()) st
for p being Point of (TOP-REAL F1()) holds
( p in A iff P1[p] )
proof
consider A being set such that
A1: for x being set holds
( x in A iff ( x in the carrier of (TOP-REAL F1()) & P1[x] ) ) from XBOOLE_0:sch_1();
A c= the carrier of (TOP-REAL F1())
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in the carrier of (TOP-REAL F1()) )
assume x in A ; ::_thesis: x in the carrier of (TOP-REAL F1())
hence x in the carrier of (TOP-REAL F1()) by A1; ::_thesis: verum
end;
then reconsider A = A as Subset of (TOP-REAL F1()) ;
take A ; ::_thesis: for p being Point of (TOP-REAL F1()) holds
( p in A iff P1[p] )
thus for p being Point of (TOP-REAL F1()) holds
( p in A iff P1[p] ) by A1; ::_thesis: verum
end;
scheme :: TOPREAL1:sch 3
TRSubsetUniq{ F1() -> Nat, P1[ set ] } :
for A, B being Subset of (TOP-REAL F1()) st ( for p being Point of (TOP-REAL F1()) holds
( p in A iff P1[p] ) ) & ( for p being Point of (TOP-REAL F1()) holds
( p in B iff P1[p] ) ) holds
A = B
proof
let A, B be Subset of (TOP-REAL F1()); ::_thesis: ( ( for p being Point of (TOP-REAL F1()) holds
( p in A iff P1[p] ) ) & ( for p being Point of (TOP-REAL F1()) holds
( p in B iff P1[p] ) ) implies A = B )
assume that
A1: for p being Point of (TOP-REAL F1()) holds
( p in A iff P1[p] ) and
A2: for p being Point of (TOP-REAL F1()) holds
( p in B iff P1[p] ) ; ::_thesis: A = B
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: B c= A
let x be set ; ::_thesis: ( x in A implies x in B )
assume A3: x in A ; ::_thesis: x in B
then P1[x] by A1;
hence x in B by A2, A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in A )
assume A4: x in B ; ::_thesis: x in A
then P1[x] by A2;
hence x in A by A1, A4; ::_thesis: verum
end;
definition
let p be Point of (TOP-REAL 2);
func north_halfline p -> Subset of (TOP-REAL 2) means :Def10: :: TOPREAL1:def 10
for x being Point of (TOP-REAL 2) holds
( x in it iff ( x `1 = p `1 & x `2 >= p `2 ) );
existence
ex b1 being Subset of (TOP-REAL 2) st
for x being Point of (TOP-REAL 2) holds
( x in b1 iff ( x `1 = p `1 & x `2 >= p `2 ) )
proof
defpred S1[ Point of (TOP-REAL 2)] means ( $1 `1 = p `1 & $1 `2 >= p `2 );
thus ex IT being Subset of (TOP-REAL 2) st
for x being Point of (TOP-REAL 2) holds
( x in IT iff S1[x] ) from TOPREAL1:sch_2(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds
( x in b1 iff ( x `1 = p `1 & x `2 >= p `2 ) ) ) & ( for x being Point of (TOP-REAL 2) holds
( x in b2 iff ( x `1 = p `1 & x `2 >= p `2 ) ) ) holds
b1 = b2
proof
defpred S1[ Point of (TOP-REAL 2)] means ( $1 `1 = p `1 & $1 `2 >= p `2 );
thus for a, b being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds
( x in a iff S1[x] ) ) & ( for x being Point of (TOP-REAL 2) holds
( x in b iff S1[x] ) ) holds
a = b from TOPREAL1:sch_3(); ::_thesis: verum
end;
func east_halfline p -> Subset of (TOP-REAL 2) means :Def11: :: TOPREAL1:def 11
for x being Point of (TOP-REAL 2) holds
( x in it iff ( x `1 >= p `1 & x `2 = p `2 ) );
existence
ex b1 being Subset of (TOP-REAL 2) st
for x being Point of (TOP-REAL 2) holds
( x in b1 iff ( x `1 >= p `1 & x `2 = p `2 ) )
proof
defpred S1[ Point of (TOP-REAL 2)] means ( $1 `1 >= p `1 & $1 `2 = p `2 );
thus ex IT being Subset of (TOP-REAL 2) st
for x being Point of (TOP-REAL 2) holds
( x in IT iff S1[x] ) from TOPREAL1:sch_2(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds
( x in b1 iff ( x `1 >= p `1 & x `2 = p `2 ) ) ) & ( for x being Point of (TOP-REAL 2) holds
( x in b2 iff ( x `1 >= p `1 & x `2 = p `2 ) ) ) holds
b1 = b2
proof
defpred S1[ Point of (TOP-REAL 2)] means ( $1 `1 >= p `1 & $1 `2 = p `2 );
thus for a, b being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds
( x in a iff S1[x] ) ) & ( for x being Point of (TOP-REAL 2) holds
( x in b iff S1[x] ) ) holds
a = b from TOPREAL1:sch_3(); ::_thesis: verum
end;
func south_halfline p -> Subset of (TOP-REAL 2) means :Def12: :: TOPREAL1:def 12
for x being Point of (TOP-REAL 2) holds
( x in it iff ( x `1 = p `1 & x `2 <= p `2 ) );
existence
ex b1 being Subset of (TOP-REAL 2) st
for x being Point of (TOP-REAL 2) holds
( x in b1 iff ( x `1 = p `1 & x `2 <= p `2 ) )
proof
defpred S1[ Point of (TOP-REAL 2)] means ( $1 `1 = p `1 & $1 `2 <= p `2 );
thus ex IT being Subset of (TOP-REAL 2) st
for x being Point of (TOP-REAL 2) holds
( x in IT iff S1[x] ) from TOPREAL1:sch_2(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds
( x in b1 iff ( x `1 = p `1 & x `2 <= p `2 ) ) ) & ( for x being Point of (TOP-REAL 2) holds
( x in b2 iff ( x `1 = p `1 & x `2 <= p `2 ) ) ) holds
b1 = b2
proof
defpred S1[ Point of (TOP-REAL 2)] means ( $1 `1 = p `1 & $1 `2 <= p `2 );
thus for a, b being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds
( x in a iff S1[x] ) ) & ( for x being Point of (TOP-REAL 2) holds
( x in b iff S1[x] ) ) holds
a = b from TOPREAL1:sch_3(); ::_thesis: verum
end;
func west_halfline p -> Subset of (TOP-REAL 2) means :Def13: :: TOPREAL1:def 13
for x being Point of (TOP-REAL 2) holds
( x in it iff ( x `1 <= p `1 & x `2 = p `2 ) );
existence
ex b1 being Subset of (TOP-REAL 2) st
for x being Point of (TOP-REAL 2) holds
( x in b1 iff ( x `1 <= p `1 & x `2 = p `2 ) )
proof
defpred S1[ Point of (TOP-REAL 2)] means ( $1 `1 <= p `1 & $1 `2 = p `2 );
thus ex IT being Subset of (TOP-REAL 2) st
for x being Point of (TOP-REAL 2) holds
( x in IT iff S1[x] ) from TOPREAL1:sch_2(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds
( x in b1 iff ( x `1 <= p `1 & x `2 = p `2 ) ) ) & ( for x being Point of (TOP-REAL 2) holds
( x in b2 iff ( x `1 <= p `1 & x `2 = p `2 ) ) ) holds
b1 = b2
proof
defpred S1[ Point of (TOP-REAL 2)] means ( $1 `1 <= p `1 & $1 `2 = p `2 );
thus for a, b being Subset of (TOP-REAL 2) st ( for x being Point of (TOP-REAL 2) holds
( x in a iff S1[x] ) ) & ( for x being Point of (TOP-REAL 2) holds
( x in b iff S1[x] ) ) holds
a = b from TOPREAL1:sch_3(); ::_thesis: verum
end;
end;
:: deftheorem Def10 defines north_halfline TOPREAL1:def_10_:_
for p being Point of (TOP-REAL 2)
for b2 being Subset of (TOP-REAL 2) holds
( b2 = north_halfline p iff for x being Point of (TOP-REAL 2) holds
( x in b2 iff ( x `1 = p `1 & x `2 >= p `2 ) ) );
:: deftheorem Def11 defines east_halfline TOPREAL1:def_11_:_
for p being Point of (TOP-REAL 2)
for b2 being Subset of (TOP-REAL 2) holds
( b2 = east_halfline p iff for x being Point of (TOP-REAL 2) holds
( x in b2 iff ( x `1 >= p `1 & x `2 = p `2 ) ) );
:: deftheorem Def12 defines south_halfline TOPREAL1:def_12_:_
for p being Point of (TOP-REAL 2)
for b2 being Subset of (TOP-REAL 2) holds
( b2 = south_halfline p iff for x being Point of (TOP-REAL 2) holds
( x in b2 iff ( x `1 = p `1 & x `2 <= p `2 ) ) );
:: deftheorem Def13 defines west_halfline TOPREAL1:def_13_:_
for p being Point of (TOP-REAL 2)
for b2 being Subset of (TOP-REAL 2) holds
( b2 = west_halfline p iff for x being Point of (TOP-REAL 2) holds
( x in b2 iff ( x `1 <= p `1 & x `2 = p `2 ) ) );
theorem :: TOPREAL1:30
for p being Point of (TOP-REAL 2) holds north_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 >= p `2 ) }
proof
let p be Point of (TOP-REAL 2); ::_thesis: north_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 >= p `2 ) }
set A = { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 >= p `2 ) } ;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 >= p `2 ) } c= north_halfline p
let x be set ; ::_thesis: ( x in north_halfline p implies x in { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 >= p `2 ) } )
assume A1: x in north_halfline p ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 >= p `2 ) }
then reconsider q = x as Point of (TOP-REAL 2) ;
A2: q `2 >= p `2 by A1, Def10;
q `1 = p `1 by A1, Def10;
hence x in { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 >= p `2 ) } by A2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 >= p `2 ) } or x in north_halfline p )
assume x in { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 >= p `2 ) } ; ::_thesis: x in north_halfline p
then ex q being Point of (TOP-REAL 2) st
( x = q & q `1 = p `1 & q `2 >= p `2 ) ;
hence x in north_halfline p by Def10; ::_thesis: verum
end;
theorem Th31: :: TOPREAL1:31
for p being Point of (TOP-REAL 2) holds north_halfline p = { |[(p `1),r]| where r is Element of REAL : r >= p `2 }
proof
let p be Point of (TOP-REAL 2); ::_thesis: north_halfline p = { |[(p `1),r]| where r is Element of REAL : r >= p `2 }
set A = { |[(p `1),r]| where r is Element of REAL : r >= p `2 } ;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { |[(p `1),r]| where r is Element of REAL : r >= p `2 } c= north_halfline p
let x be set ; ::_thesis: ( x in north_halfline p implies x in { |[(p `1),r]| where r is Element of REAL : r >= p `2 } )
assume A1: x in north_halfline p ; ::_thesis: x in { |[(p `1),r]| where r is Element of REAL : r >= p `2 }
then reconsider q = x as Point of (TOP-REAL 2) ;
A2: q `2 >= p `2 by A1, Def10;
A3: q = |[(q `1),(q `2)]| by EUCLID:53;
q `1 = p `1 by A1, Def10;
hence x in { |[(p `1),r]| where r is Element of REAL : r >= p `2 } by A2, A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[(p `1),r]| where r is Element of REAL : r >= p `2 } or x in north_halfline p )
assume x in { |[(p `1),r]| where r is Element of REAL : r >= p `2 } ; ::_thesis: x in north_halfline p
then consider r being Element of REAL such that
A4: x = |[(p `1),r]| and
A5: r >= p `2 ;
reconsider q = x as Point of (TOP-REAL 2) by A4;
A6: q `2 = r by A4, EUCLID:52;
q `1 = p `1 by A4, EUCLID:52;
hence x in north_halfline p by A5, A6, Def10; ::_thesis: verum
end;
theorem :: TOPREAL1:32
for p being Point of (TOP-REAL 2) holds east_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 >= p `1 & q `2 = p `2 ) }
proof
let p be Point of (TOP-REAL 2); ::_thesis: east_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 >= p `1 & q `2 = p `2 ) }
set A = { q where q is Point of (TOP-REAL 2) : ( q `1 >= p `1 & q `2 = p `2 ) } ;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { q where q is Point of (TOP-REAL 2) : ( q `1 >= p `1 & q `2 = p `2 ) } c= east_halfline p
let x be set ; ::_thesis: ( x in east_halfline p implies x in { q where q is Point of (TOP-REAL 2) : ( q `1 >= p `1 & q `2 = p `2 ) } )
assume A1: x in east_halfline p ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : ( q `1 >= p `1 & q `2 = p `2 ) }
then reconsider q = x as Point of (TOP-REAL 2) ;
A2: q `2 = p `2 by A1, Def11;
q `1 >= p `1 by A1, Def11;
hence x in { q where q is Point of (TOP-REAL 2) : ( q `1 >= p `1 & q `2 = p `2 ) } by A2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : ( q `1 >= p `1 & q `2 = p `2 ) } or x in east_halfline p )
assume x in { q where q is Point of (TOP-REAL 2) : ( q `1 >= p `1 & q `2 = p `2 ) } ; ::_thesis: x in east_halfline p
then ex q being Point of (TOP-REAL 2) st
( x = q & q `1 >= p `1 & q `2 = p `2 ) ;
hence x in east_halfline p by Def11; ::_thesis: verum
end;
theorem Th33: :: TOPREAL1:33
for p being Point of (TOP-REAL 2) holds east_halfline p = { |[r,(p `2)]| where r is Element of REAL : r >= p `1 }
proof
let p be Point of (TOP-REAL 2); ::_thesis: east_halfline p = { |[r,(p `2)]| where r is Element of REAL : r >= p `1 }
set A = { |[r,(p `2)]| where r is Element of REAL : r >= p `1 } ;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { |[r,(p `2)]| where r is Element of REAL : r >= p `1 } c= east_halfline p
let x be set ; ::_thesis: ( x in east_halfline p implies x in { |[r,(p `2)]| where r is Element of REAL : r >= p `1 } )
assume A1: x in east_halfline p ; ::_thesis: x in { |[r,(p `2)]| where r is Element of REAL : r >= p `1 }
then reconsider q = x as Point of (TOP-REAL 2) ;
A2: q `2 = p `2 by A1, Def11;
A3: q = |[(q `1),(q `2)]| by EUCLID:53;
q `1 >= p `1 by A1, Def11;
hence x in { |[r,(p `2)]| where r is Element of REAL : r >= p `1 } by A2, A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,(p `2)]| where r is Element of REAL : r >= p `1 } or x in east_halfline p )
assume x in { |[r,(p `2)]| where r is Element of REAL : r >= p `1 } ; ::_thesis: x in east_halfline p
then consider r being Element of REAL such that
A4: x = |[r,(p `2)]| and
A5: r >= p `1 ;
reconsider q = x as Point of (TOP-REAL 2) by A4;
A6: q `2 = p `2 by A4, EUCLID:52;
q `1 = r by A4, EUCLID:52;
hence x in east_halfline p by A5, A6, Def11; ::_thesis: verum
end;
theorem :: TOPREAL1:34
for p being Point of (TOP-REAL 2) holds south_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 <= p `2 ) }
proof
let p be Point of (TOP-REAL 2); ::_thesis: south_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 <= p `2 ) }
set A = { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 <= p `2 ) } ;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 <= p `2 ) } c= south_halfline p
let x be set ; ::_thesis: ( x in south_halfline p implies x in { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 <= p `2 ) } )
assume A1: x in south_halfline p ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 <= p `2 ) }
then reconsider q = x as Point of (TOP-REAL 2) ;
A2: q `2 <= p `2 by A1, Def12;
q `1 = p `1 by A1, Def12;
hence x in { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 <= p `2 ) } by A2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 <= p `2 ) } or x in south_halfline p )
assume x in { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 <= p `2 ) } ; ::_thesis: x in south_halfline p
then ex q being Point of (TOP-REAL 2) st
( x = q & q `1 = p `1 & q `2 <= p `2 ) ;
hence x in south_halfline p by Def12; ::_thesis: verum
end;
theorem Th35: :: TOPREAL1:35
for p being Point of (TOP-REAL 2) holds south_halfline p = { |[(p `1),r]| where r is Element of REAL : r <= p `2 }
proof
let p be Point of (TOP-REAL 2); ::_thesis: south_halfline p = { |[(p `1),r]| where r is Element of REAL : r <= p `2 }
set A = { |[(p `1),r]| where r is Element of REAL : r <= p `2 } ;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { |[(p `1),r]| where r is Element of REAL : r <= p `2 } c= south_halfline p
let x be set ; ::_thesis: ( x in south_halfline p implies x in { |[(p `1),r]| where r is Element of REAL : r <= p `2 } )
assume A1: x in south_halfline p ; ::_thesis: x in { |[(p `1),r]| where r is Element of REAL : r <= p `2 }
then reconsider q = x as Point of (TOP-REAL 2) ;
A2: q `2 <= p `2 by A1, Def12;
A3: q = |[(q `1),(q `2)]| by EUCLID:53;
q `1 = p `1 by A1, Def12;
hence x in { |[(p `1),r]| where r is Element of REAL : r <= p `2 } by A2, A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[(p `1),r]| where r is Element of REAL : r <= p `2 } or x in south_halfline p )
assume x in { |[(p `1),r]| where r is Element of REAL : r <= p `2 } ; ::_thesis: x in south_halfline p
then consider r being Element of REAL such that
A4: x = |[(p `1),r]| and
A5: r <= p `2 ;
reconsider q = x as Point of (TOP-REAL 2) by A4;
A6: q `2 = r by A4, EUCLID:52;
q `1 = p `1 by A4, EUCLID:52;
hence x in south_halfline p by A5, A6, Def12; ::_thesis: verum
end;
theorem :: TOPREAL1:36
for p being Point of (TOP-REAL 2) holds west_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 <= p `1 & q `2 = p `2 ) }
proof
let p be Point of (TOP-REAL 2); ::_thesis: west_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 <= p `1 & q `2 = p `2 ) }
set A = { q where q is Point of (TOP-REAL 2) : ( q `1 <= p `1 & q `2 = p `2 ) } ;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { q where q is Point of (TOP-REAL 2) : ( q `1 <= p `1 & q `2 = p `2 ) } c= west_halfline p
let x be set ; ::_thesis: ( x in west_halfline p implies x in { q where q is Point of (TOP-REAL 2) : ( q `1 <= p `1 & q `2 = p `2 ) } )
assume A1: x in west_halfline p ; ::_thesis: x in { q where q is Point of (TOP-REAL 2) : ( q `1 <= p `1 & q `2 = p `2 ) }
then reconsider q = x as Point of (TOP-REAL 2) ;
A2: q `2 = p `2 by A1, Def13;
q `1 <= p `1 by A1, Def13;
hence x in { q where q is Point of (TOP-REAL 2) : ( q `1 <= p `1 & q `2 = p `2 ) } by A2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Point of (TOP-REAL 2) : ( q `1 <= p `1 & q `2 = p `2 ) } or x in west_halfline p )
assume x in { q where q is Point of (TOP-REAL 2) : ( q `1 <= p `1 & q `2 = p `2 ) } ; ::_thesis: x in west_halfline p
then ex q being Point of (TOP-REAL 2) st
( x = q & q `1 <= p `1 & q `2 = p `2 ) ;
hence x in west_halfline p by Def13; ::_thesis: verum
end;
theorem Th37: :: TOPREAL1:37
for p being Point of (TOP-REAL 2) holds west_halfline p = { |[r,(p `2)]| where r is Element of REAL : r <= p `1 }
proof
let p be Point of (TOP-REAL 2); ::_thesis: west_halfline p = { |[r,(p `2)]| where r is Element of REAL : r <= p `1 }
set A = { |[r,(p `2)]| where r is Element of REAL : r <= p `1 } ;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { |[r,(p `2)]| where r is Element of REAL : r <= p `1 } c= west_halfline p
let x be set ; ::_thesis: ( x in west_halfline p implies x in { |[r,(p `2)]| where r is Element of REAL : r <= p `1 } )
assume A1: x in west_halfline p ; ::_thesis: x in { |[r,(p `2)]| where r is Element of REAL : r <= p `1 }
then reconsider q = x as Point of (TOP-REAL 2) ;
A2: q `2 = p `2 by A1, Def13;
A3: q = |[(q `1),(q `2)]| by EUCLID:53;
q `1 <= p `1 by A1, Def13;
hence x in { |[r,(p `2)]| where r is Element of REAL : r <= p `1 } by A2, A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { |[r,(p `2)]| where r is Element of REAL : r <= p `1 } or x in west_halfline p )
assume x in { |[r,(p `2)]| where r is Element of REAL : r <= p `1 } ; ::_thesis: x in west_halfline p
then consider r being Element of REAL such that
A4: x = |[r,(p `2)]| and
A5: r <= p `1 ;
reconsider q = x as Point of (TOP-REAL 2) by A4;
A6: q `2 = p `2 by A4, EUCLID:52;
q `1 = r by A4, EUCLID:52;
hence x in west_halfline p by A5, A6, Def13; ::_thesis: verum
end;
registration
let p be Point of (TOP-REAL 2);
cluster north_halfline p -> non empty ;
coherence
not north_halfline p is empty
proof
north_halfline p = { |[(p `1),r]| where r is Element of REAL : r >= p `2 } by Th31;
then |[(p `1),(p `2)]| in north_halfline p ;
hence not north_halfline p is empty ; ::_thesis: verum
end;
cluster east_halfline p -> non empty ;
coherence
not east_halfline p is empty
proof
east_halfline p = { |[r,(p `2)]| where r is Element of REAL : r >= p `1 } by Th33;
then |[(p `1),(p `2)]| in east_halfline p ;
hence not east_halfline p is empty ; ::_thesis: verum
end;
cluster south_halfline p -> non empty ;
coherence
not south_halfline p is empty
proof
south_halfline p = { |[(p `1),r]| where r is Element of REAL : r <= p `2 } by Th35;
then |[(p `1),(p `2)]| in south_halfline p ;
hence not south_halfline p is empty ; ::_thesis: verum
end;
cluster west_halfline p -> non empty ;
coherence
not west_halfline p is empty
proof
west_halfline p = { |[r,(p `2)]| where r is Element of REAL : r <= p `1 } by Th37;
then |[(p `1),(p `2)]| in west_halfline p ;
hence not west_halfline p is empty ; ::_thesis: verum
end;
end;
theorem :: TOPREAL1:38
for p being Point of (TOP-REAL 2) holds
( p in west_halfline p & p in east_halfline p & p in north_halfline p & p in south_halfline p )
proof
let p be Point of (TOP-REAL 2); ::_thesis: ( p in west_halfline p & p in east_halfline p & p in north_halfline p & p in south_halfline p )
A1: p `2 = p `2 ;
p `1 <= p `1 ;
hence ( p in west_halfline p & p in east_halfline p & p in north_halfline p & p in south_halfline p ) by A1, Def10, Def11, Def12, Def13; ::_thesis: verum
end;