:: TOPREAL1 semantic presentation

Lm1: for n being Nat holds
( the carrier of (Euclid n) = REAL n & the carrier of (TOP-REAL n) = REAL n )
by TOPMETR:16;

scheme :: TOPREAL1:sch 1
FraenkelAlt{ F₁() -> non empty set , P₁[ set ], P₂[ set ] } :

{ v where v is Element of F₁() : ( P₁[v] or P₂[v] ) } = { v1 where v1 is Element of F₁() : P₁[v1] } \/ { v2 where v2 is Element of F₁() : P₂[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[01] ,(T | P) st
( f is_homeomorphism & f . 0 = p1 & f . 1 = p2 );

end;

:: deftheorem TOPREAL1:def 1 :

:: deftheorem Def2 defines is_an_arc_of TOPREAL1:def 2 :

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 being_T2 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

let n be Nat;
let p1, p2 be Point of (TOP-REAL n);
func LSeg p1,p2 -> Subset of (TOP-REAL n) equals :Def3: :: TOPREAL1:def 3
{ (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } ;
coherence

proof end;

end;

:: deftheorem Def3 defines LSeg TOPREAL1:def 3 :

definition

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

end;

:: deftheorem defines R^2-unit_square TOPREAL1:def 4 :

registration

let n be Nat;
let p1, p2 be Point of (TOP-REAL n);
cluster LSeg p1,p2 -> non empty ;
coherence

proof end;

end;

theorem Th6: :: TOPREAL1:6

for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds
( p1 in LSeg p1,p2 & p2 in LSeg p1,p2 )

proof end;

theorem Th7: :: TOPREAL1:7

for n being Nat
for p being Point of (TOP-REAL n) holds LSeg p,p = {p}

proof end;

theorem Th8: :: TOPREAL1:8

for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds LSeg p1,p2 = LSeg p2,p1

proof end;

definition

let n be Nat;
let p1, p2 be Point of (TOP-REAL n);
:: original: LSeg
redefine func LSeg p1,p2 -> Subset of (TOP-REAL n);
commutativity by Th8;

end;

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

theorem :: TOPREAL1:9

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

theorem :: TOPREAL1:10

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

theorem Th11: :: TOPREAL1:11

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

theorem Th12: :: TOPREAL1:12

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

theorem :: TOPREAL1:13

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

theorem :: TOPREAL1:14

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

theorem Th15: :: TOPREAL1:15

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

registration

let n be Nat;
cluster TOP-REAL n -> being_T2 ;
coherence by PCOMPS_1:38;

end;

theorem Th16: :: TOPREAL1:16

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

theorem Th17: :: TOPREAL1:17

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

theorem :: TOPREAL1:18

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

theorem Th19: :: TOPREAL1:19

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

theorem :: TOPREAL1:20

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

registration

cluster R^2-unit_square -> non empty ;
coherence

proof end;

end;

theorem :: TOPREAL1:21

(LSeg |[0,0]|,|[0,1]|) /\ (LSeg |[0,1]|,|[1,1]|) = {|[0,1]|}

proof end;

theorem :: TOPREAL1:22

(LSeg |[0,0]|,|[1,0]|) /\ (LSeg |[1,0]|,|[1,1]|) = {|[1,0]|}

proof end;

theorem Th23: :: TOPREAL1:23

(LSeg |[0,0]|,|[0,1]|) /\ (LSeg |[0,0]|,|[1,0]|) = {|[0,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 |[0,0]|,|[1,0]| misses LSeg |[0,1]|,|[1,1]|

proof end;

theorem Th26: :: TOPREAL1:26

LSeg |[0,0]|,|[0,1]| misses LSeg |[1,0]|,|[1,1]|

proof 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 :Def5: :: TOPREAL1:def 5
LSeg (f /. i),(f /. (i + 1)) if ( 1 <= i & i + 1 <= len f )
otherwise {} ;
coherence

proof end;

correctness ;

end;

:: deftheorem Def5 defines LSeg TOPREAL1:def 5 :

theorem Th27: :: TOPREAL1:27

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 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 6
union { (LSeg f,i) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;
coherence

proof end;

end;

:: deftheorem defines L~ TOPREAL1:def 6 :

theorem Th28: :: TOPREAL1:28

for n being Nat
for f being FinSequence of (TOP-REAL n) 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 (TOP-REAL n) st len f >= 2 holds
L~ f <> {}

proof end;

definition

let IT be FinSequence of (TOP-REAL 2);
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 :

:: deftheorem Def8 defines unfolded TOPREAL1:def 8 :

:: deftheorem Def9 defines s.n.c. TOPREAL1:def 9 :

definition

let f be FinSequence of (TOP-REAL 2);
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 :

notation

let f be FinSequence of (TOP-REAL 2);
synonym f is_S-Seq for being_S-Seq f;

end;

theorem Th30: :: TOPREAL1:30

ex f1, f2 being FinSequence of (TOP-REAL 2) st
( f1 is_S-Seq & f2 is_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 end;

theorem Th31: :: TOPREAL1:31

for h being FinSequence of (TOP-REAL 2) st h is_S-Seq holds
L~ h is_an_arc_of h /. 1,h /. (len h)

proof end;

definition

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

end;

:: deftheorem Def11 defines being_S-P_arc TOPREAL1:def 11 :

notation

let P be Subset of (TOP-REAL 2);
synonym P is_S-P_arc for being_S-P_arc P;

end;

theorem Th32: :: TOPREAL1:32

for P1 being Subset of (TOP-REAL 2) st P1 is_S-P_arc holds
P1 <> {}

proof end;

registration

cluster being_S-P_arc -> non empty Element of K40(the carrier of (TOP-REAL 2));
coherence by Th32;

end;

theorem :: TOPREAL1:33

canceled;

theorem :: TOPREAL1:34

ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_S-P_arc & P2 is_S-P_arc & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {|[0,0]|,|[1,1]|} )

proof end;

theorem Th35: :: TOPREAL1:35

for P being Subset of (TOP-REAL 2) st P is_S-P_arc holds
ex p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2

proof end;

theorem :: TOPREAL1:36

for P being Subset of (TOP-REAL 2) st P is_S-P_arc holds
ex f being Function of I[01] ,((TOP-REAL 2) | P) st f is_homeomorphism

proof end;