:: The Topological Space ${\calE}^2_{\rm T}$. Arcs, Line Segments and Special Polygonal Arcs
:: by Agata Darmochwa{\l} and Yatsuka Nakamura
::
:: Copyright (c) 1991 Association of Mizar Users

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 end;

definition
let T be TopSpace;
let p1, p2 be Point of T;
let P be Subset of T;
canceled;
pred P is_an_arc_of p1,p2 means :Def2: :: TOPREAL1:def 2
ex f being Function of I,(T | P) st
( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 );
end;

:: 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,(T | P) st
( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) );

theorem :: TOPREAL1:1
canceled;

theorem :: TOPREAL1:2
canceled;

theorem :: TOPREAL1:3
canceled;

theorem Th4: :: TOPREAL1:4
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 end;

theorem Th5: :: TOPREAL1:5
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 end;

definition
canceled;
func R^2-unit_square -> Subset of () equals :: TOPREAL1:def 4
((LSeg (,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,)));
coherence
((LSeg (,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,))) is Subset of ()
;
end;

:: deftheorem TOPREAL1:def 3 :
canceled;

:: deftheorem defines R^2-unit_square TOPREAL1:def 4 :
R^2-unit_square = ((LSeg (,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,)));

theorem :: TOPREAL1:6
canceled;

theorem :: TOPREAL1:7
canceled;

Lm1: for n being Nat
for p, p1, p2 being Point of () st p in LSeg (p1,p2) holds
LSeg (p1,p) c= LSeg (p1,p2)
proof end;

theorem :: TOPREAL1:8
canceled;

theorem :: TOPREAL1:9
for p1, p2, p being Point of () st p1 1 <= p2 1 & p in LSeg (p1,p2) holds
( p1 1 <= p 1 & p 1 <= p2 1 )
proof end;

theorem :: TOPREAL1:10
for p1, p2, p being Point of () st p1 2 <= p2 2 & p in LSeg (p1,p2) holds
( p1 2 <= p 2 & p 2 <= p2 2 )
proof end;

theorem Th11: :: TOPREAL1:11
for n being Nat
for p, p1, p2 being Point of () st p in LSeg (p1,p2) holds
LSeg (p1,p2) = (LSeg (p1,p)) \/ (LSeg (p,p2))
proof end;

theorem Th12: :: TOPREAL1:12
for n being Nat
for p1, p2, q1, q2 being Point of () st q1 in LSeg (p1,p2) & q2 in LSeg (p1,p2) holds
LSeg (q1,q2) c= LSeg (p1,p2)
proof end;

theorem :: TOPREAL1:13
for n being Nat
for p, q, p1, p2 being Point of () 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 end;

theorem :: TOPREAL1:14
for n being Nat
for p, p1, p2 being Point of () st p in LSeg (p1,p2) holds
(LSeg (p1,p)) /\ (LSeg (p,p2)) = {p}
proof 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 end;

registration
let n be Nat;
cluster -> Relation-like Function-like Element of the carrier of ();
coherence
for b1 being Point of () holds
( b1 is Function-like & b1 is Relation-like )
by EUCLID:26;
end;

theorem Th15: :: TOPREAL1:15
for n being Nat
for p1, p2 being Point of () st p1 <> p2 holds
LSeg (p1,p2) is_an_arc_of p1,p2
proof end;

registration
let n be Nat;
cluster TOP-REAL n -> T_2 ;
coherence
TOP-REAL n is T_2
proof end;
end;

theorem Th16: :: TOPREAL1:16
for n being Nat
for P being Subset of ()
for p1, p2, q1 being Point of () 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 end;

theorem Th17: :: TOPREAL1:17
for n being Nat
for P being Subset of ()
for p1, p2, q1 being Point of () 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 end;

theorem :: TOPREAL1:18
for n being Nat
for p1, p2, q1 being Point of () 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 end;

theorem Th19: :: TOPREAL1:19
( LSeg (,|[0,1]|) = { p1 where p1 is Point of () : ( p1 1 = 0 & p1 2 <= 1 & p1 2 >= 0 ) } & LSeg (|[0,1]|,|[1,1]|) = { p2 where p2 is Point of () : ( p2 1 <= 1 & p2 1 >= 0 & p2 2 = 1 ) } & LSeg (,|[1,0]|) = { q1 where q1 is Point of () : ( q1 1 <= 1 & q1 1 >= 0 & q1 2 = 0 ) } & LSeg (|[1,0]|,|[1,1]|) = { q2 where q2 is Point of () : ( q2 1 = 1 & q2 2 <= 1 & q2 2 >= 0 ) } )
proof end;

theorem :: TOPREAL1:20
R^2-unit_square = { p where p is Point of () : ( ( 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 end;

registration
cluster R^2-unit_square -> non empty ;
coherence
not R^2-unit_square is empty
;
end;

theorem :: TOPREAL1:21
(LSeg (,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {|[0,1]|}
proof end;

theorem :: TOPREAL1:22
(LSeg (,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {|[1,0]|}
proof end;

theorem Th23: :: TOPREAL1:23
(LSeg (,|[0,1]|)) /\ (LSeg (,|[1,0]|)) =
proof end;

theorem Th24: :: TOPREAL1:24
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {|[1,1]|}
proof end;

theorem :: TOPREAL1:25
LSeg (,|[1,0]|) misses LSeg (|[0,1]|,|[1,1]|)
proof end;

theorem Th26: :: TOPREAL1:26
LSeg (,|[0,1]|) misses LSeg (|[1,0]|,|[1,1]|)
proof end;

definition
let n be Nat;
let f be FinSequence of ();
let i be Nat;
func LSeg (f,i) -> Subset of () equals :Def5: :: TOPREAL1:def 5
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 () ) & ( ( not 1 <= i or not i + 1 <= len f ) implies {} is Subset of () ) )
proof end;
correctness
consistency
for b1 being Subset of () holds verum
;
;
end;

:: deftheorem Def5 defines LSeg TOPREAL1:def 5 :
for n being Nat
for f being FinSequence of ()
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: :: TOPREAL1:27
for n, i being Nat
for f being FinSequence of () st 1 <= i & i + 1 <= len f holds
( f /. i in LSeg (f,i) & f /. (i + 1) in LSeg (f,i) )
proof end;

definition
let n be Nat;
let f be FinSequence of ();
func L~ f -> Subset of () equals :: TOPREAL1:def 6
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 ()
proof end;
end;

:: deftheorem defines L~ TOPREAL1:def 6 :
for n being Nat
for f being FinSequence of () holds L~ f = union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ;

theorem Th28: :: TOPREAL1:28
for n being Nat
for f being FinSequence of () holds
( ( len f = 0 or len f = 1 ) iff L~ f = {} )
proof end;

theorem Th29: :: TOPREAL1:29
for n being Nat
for f being FinSequence of () st len f >= 2 holds
L~ f <> {}
proof end;

definition
let IT be FinSequence of ();
attr IT is special means :: TOPREAL1:def 7
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 ;
attr IT is unfolded means :Def8: :: TOPREAL1:def 8
for i being Nat st 1 <= i & i + 2 <= len IT holds
(LSeg (IT,i)) /\ (LSeg (IT,(i + 1))) = {(IT /. (i + 1))};
attr IT is s.n.c. means :Def9: :: TOPREAL1:def 9
for i, j being Nat st i + 1 < j holds
LSeg (IT,i) misses LSeg (IT,j);
end;

:: deftheorem defines special TOPREAL1:def 7 :
for IT being FinSequence of () 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 () 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 () 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 ();
attr f is being_S-Seq means :Def10: :: TOPREAL1:def 10
( f is one-to-one & len f >= 2 & f is unfolded & f is s.n.c. & f is special );
end;

:: deftheorem Def10 defines being_S-Seq TOPREAL1:def 10 :
for f being FinSequence of () 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: :: TOPREAL1:30
ex f1, f2 being FinSequence of () st
( f1 is being_S-Seq & f2 is being_S-Seq & R^2-unit_square = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {,|[1,1]|} & f1 /. 1 = & f1 /. (len f1) = |[1,1]| & f2 /. 1 = & f2 /. (len f2) = |[1,1]| )
proof end;

theorem Th31: :: TOPREAL1:31
for h being FinSequence of () st h is being_S-Seq holds
L~ h is_an_arc_of h /. 1,h /. (len h)
proof end;

definition
let P be Subset of ();
attr P is being_S-P_arc means :Def11: :: TOPREAL1:def 11
ex f being FinSequence of () st
( f is being_S-Seq & P = L~ f );
end;

:: deftheorem Def11 defines being_S-P_arc TOPREAL1:def 11 :
for P being Subset of () holds
( P is being_S-P_arc iff ex f being FinSequence of () st
( f is being_S-Seq & P = L~ f ) );

theorem Th32: :: TOPREAL1:32
for P1 being Subset of () st P1 is being_S-P_arc holds
P1 <> {}
proof end;

registration
cluster being_S-P_arc -> non empty Element of K10( the carrier of ());
coherence
for b1 being Subset of () st b1 is being_S-P_arc holds
not b1 is empty
by Th32;
end;

theorem :: TOPREAL1:33
canceled;

theorem :: TOPREAL1:34
ex P1, P2 being non empty Subset of () st
( P1 is being_S-P_arc & P2 is being_S-P_arc & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {,|[1,1]|} )
proof end;

theorem Th35: :: TOPREAL1:35
for P being Subset of () st P is being_S-P_arc holds
ex p1, p2 being Point of () st P is_an_arc_of p1,p2
proof end;

theorem :: TOPREAL1:36
for P being Subset of () st P is being_S-P_arc holds
ex f being Function of I,(() | P) st f is being_homeomorphism
proof 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 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 end;

definition
let p be Point of ();
func north_halfline p -> Subset of () means :Def12: :: TOPREAL1:def 12
for x being Point of () holds
( x in it iff ( x 1 = p 1 & x 2 >= p 2 ) );
existence
ex b1 being Subset of () st
for x being Point of () holds
( x in b1 iff ( x 1 = p 1 & x 2 >= p 2 ) )
proof end;
uniqueness
for b1, b2 being Subset of () st ( for x being Point of () holds
( x in b1 iff ( x 1 = p 1 & x 2 >= p 2 ) ) ) & ( for x being Point of () holds
( x in b2 iff ( x 1 = p 1 & x 2 >= p 2 ) ) ) holds
b1 = b2
proof end;
func east_halfline p -> Subset of () means :Def13: :: TOPREAL1:def 13
for x being Point of () holds
( x in it iff ( x 1 >= p 1 & x 2 = p 2 ) );
existence
ex b1 being Subset of () st
for x being Point of () holds
( x in b1 iff ( x 1 >= p 1 & x 2 = p 2 ) )
proof end;
uniqueness
for b1, b2 being Subset of () st ( for x being Point of () holds
( x in b1 iff ( x 1 >= p 1 & x 2 = p 2 ) ) ) & ( for x being Point of () holds
( x in b2 iff ( x 1 >= p 1 & x 2 = p 2 ) ) ) holds
b1 = b2
proof end;
func south_halfline p -> Subset of () means :Def14: :: TOPREAL1:def 14
for x being Point of () holds
( x in it iff ( x 1 = p 1 & x 2 <= p 2 ) );
existence
ex b1 being Subset of () st
for x being Point of () holds
( x in b1 iff ( x 1 = p 1 & x 2 <= p 2 ) )
proof end;
uniqueness
for b1, b2 being Subset of () st ( for x being Point of () holds
( x in b1 iff ( x 1 = p 1 & x 2 <= p 2 ) ) ) & ( for x being Point of () holds
( x in b2 iff ( x 1 = p 1 & x 2 <= p 2 ) ) ) holds
b1 = b2
proof end;
func west_halfline p -> Subset of () means :Def15: :: TOPREAL1:def 15
for x being Point of () holds
( x in it iff ( x 1 <= p 1 & x 2 = p 2 ) );
existence
ex b1 being Subset of () st
for x being Point of () holds
( x in b1 iff ( x 1 <= p 1 & x 2 = p 2 ) )
proof end;
uniqueness
for b1, b2 being Subset of () st ( for x being Point of () holds
( x in b1 iff ( x 1 <= p 1 & x 2 = p 2 ) ) ) & ( for x being Point of () holds
( x in b2 iff ( x 1 <= p 1 & x 2 = p 2 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines north_halfline TOPREAL1:def 12 :
for p being Point of ()
for b2 being Subset of () holds
( b2 = north_halfline p iff for x being Point of () 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 ()
for b2 being Subset of () holds
( b2 = east_halfline p iff for x being Point of () 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 ()
for b2 being Subset of () holds
( b2 = south_halfline p iff for x being Point of () 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 ()
for b2 being Subset of () holds
( b2 = west_halfline p iff for x being Point of () holds
( x in b2 iff ( x 1 <= p 1 & x 2 = p 2 ) ) );

theorem :: TOPREAL1:37
for p being Point of () holds north_halfline p = { q where q is Point of () : ( q 1 = p 1 & q 2 >= p 2 ) }
proof end;

theorem Th38: :: TOPREAL1:38
for p being Point of () holds north_halfline p = { |[(p 1),r]| where r is Element of REAL : r >= p 2 }
proof end;

theorem :: TOPREAL1:39
for p being Point of () holds east_halfline p = { q where q is Point of () : ( q 1 >= p 1 & q 2 = p 2 ) }
proof end;

theorem Th40: :: TOPREAL1:40
for p being Point of () holds east_halfline p = { |[r,(p 2)]| where r is Element of REAL : r >= p 1 }
proof end;

theorem :: TOPREAL1:41
for p being Point of () holds south_halfline p = { q where q is Point of () : ( q 1 = p 1 & q 2 <= p 2 ) }
proof end;

theorem Th42: :: TOPREAL1:42
for p being Point of () holds south_halfline p = { |[(p 1),r]| where r is Element of REAL : r <= p 2 }
proof end;

theorem :: TOPREAL1:43
for p being Point of () holds west_halfline p = { q where q is Point of () : ( q 1 <= p 1 & q 2 = p 2 ) }
proof end;

theorem Th44: :: TOPREAL1:44
for p being Point of () holds west_halfline p = { |[r,(p 2)]| where r is Element of REAL : r <= p 1 }
proof end;

registration
let p be Point of ();
cluster north_halfline p -> non empty ;
coherence
not north_halfline p is empty
proof end;
cluster east_halfline p -> non empty ;
coherence
not east_halfline p is empty
proof end;
cluster south_halfline p -> non empty ;
coherence
not south_halfline p is empty
proof end;
cluster west_halfline p -> non empty ;
coherence
not west_halfline p is empty
proof end;
end;

theorem :: TOPREAL1:45
for p being Point of () holds
( p in west_halfline p & p in east_halfline p & p in north_halfline p & p in south_halfline p )
proof end;