begin
:: deftheorem TOPREAL1:def 1 :
canceled;
:: deftheorem Def2 defines is_an_arc_of TOPREAL1:def 2 :
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
canceled;
theorem
canceled;
theorem
canceled;
theorem Th4:
theorem Th5:
definition
canceled;func R^2-unit_square -> Subset of
(TOP-REAL 2) equals
((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 TOPREAL1:def 3 :
canceled;
:: deftheorem defines R^2-unit_square TOPREAL1:def 4 :
R^2-unit_square = ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg |[1,1]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[0 ,0 ]|));
theorem
canceled;
theorem
canceled;
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
theorem
canceled;
theorem
theorem
theorem Th11:
theorem Th12:
theorem
theorem
Lm2:
for T being TopSpace holds
( T is T_2 iff TopStruct(# the carrier of T,the topology of T #) is T_2 )
theorem Th15:
theorem Th16:
theorem Th17:
theorem
theorem Th19:
(
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 ) } )
theorem
theorem
theorem
theorem Th23:
theorem Th24:
theorem
theorem Th26:
:: deftheorem Def5 defines LSeg TOPREAL1:def 5 :
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 Th27:
:: deftheorem defines L~ TOPREAL1:def 6 :
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 Th28:
theorem Th29:
:: deftheorem defines special TOPREAL1:def 7 :
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 Def8 defines unfolded TOPREAL1:def 8 :
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 Def9 defines s.n.c. TOPREAL1:def 9 :
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 );
:: deftheorem Def10 defines being_S-Seq TOPREAL1:def 10 :
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 Th30:
theorem Th31:
:: deftheorem Def11 defines being_S-P_arc TOPREAL1:def 11 :
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 Th32:
theorem
canceled;
theorem
theorem Th35:
theorem
:: deftheorem Def12 defines north_halfline TOPREAL1:def 12 :
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 Def13 defines east_halfline TOPREAL1:def 13 :
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 Def14 defines south_halfline TOPREAL1:def 14 :
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 Def15 defines west_halfline TOPREAL1:def 15 :
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
theorem Th38:
theorem
theorem Th40:
theorem
theorem Th42:
theorem
theorem Th44:
theorem