:: TOPREAL1 semantic presentation

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

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

{ b₁ where B is Element of F₁() : ( P₁[b₁] or P₂[b₁] ) } = { b₁ where B is Element of F₁() : P₁[b₁] } \/ { b₁ where B is Element of F₁() : P₂[b₁] }

proof end;

definition

let c₁ be TopSpace;
let c₂, c₃ be Point of c₁;
let c₄ be Subset of c₁;
canceled;
pred c₄ is_an_arc_of c₂,c₃ means :Def2: :: TOPREAL1:def 2
ex b₁ being Function of I[01] ,(a₁ | a₄) st
( b₁ is_homeomorphism & b₁ . 0 = a₂ & b₁ . 1 = a₃ );

end;

:: deftheorem Def1 TOPREAL1:def 1 :

:: deftheorem Def2 defines is_an_arc_of TOPREAL1:def 2 :

theorem Th1: :: TOPREAL1:1

canceled;

theorem Th2: :: TOPREAL1:2

canceled;

theorem Th3: :: TOPREAL1:3

canceled;

theorem Th4: :: TOPREAL1:4

for b₁ being TopSpace
for b₂ being Subset of b₁
for b₃, b₄ being Point of b₁ st b₂ is_an_arc_of b₃,b₄ holds
( b₃ in b₂ & b₄ in b₂ )

proof end;

theorem Th5: :: TOPREAL1:5

for b₁ being being_T2 TopSpace
for b₂, b₃ being Subset of b₁
for b₄, b₅, b₆ being Point of b₁ st b₂ is_an_arc_of b₄,b₅ & b₃ is_an_arc_of b₅,b₆ & b₂ /\ b₃ = {b₅} holds
b₂ \/ b₃ is_an_arc_of b₄,b₆

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Point of (TOP-REAL c₁);
func LSeg c₂,c₃ -> Subset of (TOP-REAL a₁) equals :Def3: :: TOPREAL1:def 3
{ (((1 - b₁) * a₂) + (b₁ * a₃)) where B is Real : ( 0 <= b₁ & b₁ <= 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 Def4 defines R^2-unit_square TOPREAL1:def 4 :

registration

let c₁ be Nat;
let c₂, c₃ be Point of (TOP-REAL c₁);
cluster LSeg a₂,a₃ -> non empty ;
coherence

proof end;

end;

theorem Th6: :: TOPREAL1:6

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds
( b₂ in LSeg b₂,b₃ & b₃ in LSeg b₂,b₃ )

proof end;

theorem Th7: :: TOPREAL1:7

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds LSeg b₂,b₂ = {b₂}

proof end;

theorem Th8: :: TOPREAL1:8

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds LSeg b₂,b₃ = LSeg b₃,b₂

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Point of (TOP-REAL c₁);
redefine func LSeg as LSeg c₂,c₃ -> Subset of (TOP-REAL a₁);
commutativity by Th8;

end;

Lemma9: for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁) st b₂ in LSeg b₃,b₄ holds
LSeg b₃,b₂ c= LSeg b₃,b₄

proof end;

theorem Th9: :: TOPREAL1:9

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st b₁ `1 <= b₂ `1 & b₃ in LSeg b₁,b₂ holds
( b₁ `1 <= b₃ `1 & b₃ `1 <= b₂ `1 )

proof end;

theorem Th10: :: TOPREAL1:10

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st b₁ `2 <= b₂ `2 & b₃ in LSeg b₁,b₂ holds
( b₁ `2 <= b₃ `2 & b₃ `2 <= b₂ `2 )

proof end;

theorem Th11: :: TOPREAL1:11

for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁) st b₂ in LSeg b₃,b₄ holds
LSeg b₃,b₄ = (LSeg b₃,b₂) \/ (LSeg b₂,b₄)

proof end;

theorem Th12: :: TOPREAL1:12

for b₁ being Nat
for b₂, b₃, b₄, b₅ being Point of (TOP-REAL b₁) st b₄ in LSeg b₂,b₃ & b₅ in LSeg b₂,b₃ holds
LSeg b₄,b₅ c= LSeg b₂,b₃

proof end;

theorem Th13: :: TOPREAL1:13

for b₁ being Nat
for b₂, b₃, b₄, b₅ being Point of (TOP-REAL b₁) st b₂ in LSeg b₄,b₅ & b₃ in LSeg b₄,b₅ holds
LSeg b₄,b₅ = ((LSeg b₄,b₂) \/ (LSeg b₂,b₃)) \/ (LSeg b₃,b₅)

proof end;

theorem Th14: :: TOPREAL1:14

for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁) st b₂ in LSeg b₃,b₄ holds
(LSeg b₃,b₂) /\ (LSeg b₂,b₄) = {b₂}

proof end;

theorem Th15: :: TOPREAL1:15

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) st b₂ <> b₃ holds
LSeg b₂,b₃ is_an_arc_of b₂,b₃

proof end;

registration

let c₁ be Nat;
cluster TOP-REAL a₁ -> being_T2 ;
coherence by PCOMPS_1:38;

end;

theorem Th16: :: TOPREAL1:16

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄, b₅ being Point of (TOP-REAL b₁) st b₂ is_an_arc_of b₃,b₄ & b₂ /\ (LSeg b₄,b₅) = {b₄} holds
b₂ \/ (LSeg b₄,b₅) is_an_arc_of b₃,b₅

proof end;

theorem Th17: :: TOPREAL1:17

for b₁ being Nat
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄, b₅ being Point of (TOP-REAL b₁) st b₂ is_an_arc_of b₄,b₃ & (LSeg b₅,b₄) /\ b₂ = {b₄} holds
(LSeg b₅,b₄) \/ b₂ is_an_arc_of b₅,b₃

proof end;

theorem Th18: :: TOPREAL1:18

for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁) st ( b₂ <> b₃ or b₃ <> b₄ ) & (LSeg b₂,b₃) /\ (LSeg b₃,b₄) = {b₃} holds
(LSeg b₂,b₃) \/ (LSeg b₃,b₄) is_an_arc_of b₂,b₄

proof end;

theorem Th19: :: TOPREAL1:19

( LSeg |[0,0]|,|[0,1]| = { b₁ where B is Point of (TOP-REAL 2) : ( b₁ `1 = 0 & b₁ `2 <= 1 & b₁ `2 >= 0 ) } & LSeg |[0,1]|,|[1,1]| = { b₁ where B is Point of (TOP-REAL 2) : ( b₁ `1 <= 1 & b₁ `1 >= 0 & b₁ `2 = 1 ) } & LSeg |[0,0]|,|[1,0]| = { b₁ where B is Point of (TOP-REAL 2) : ( b₁ `1 <= 1 & b₁ `1 >= 0 & b₁ `2 = 0 ) } & LSeg |[1,0]|,|[1,1]| = { b₁ where B is Point of (TOP-REAL 2) : ( b₁ `1 = 1 & b₁ `2 <= 1 & b₁ `2 >= 0 ) } )

proof end;

theorem Th20: :: TOPREAL1:20

R^2-unit_square = { b₁ where B is Point of (TOP-REAL 2) : ( ( b₁ `1 = 0 & b₁ `2 <= 1 & b₁ `2 >= 0 ) or ( b₁ `1 <= 1 & b₁ `1 >= 0 & b₁ `2 = 1 ) or ( b₁ `1 <= 1 & b₁ `1 >= 0 & b₁ `2 = 0 ) or ( b₁ `1 = 1 & b₁ `2 <= 1 & b₁ `2 >= 0 ) ) }

proof end;

registration

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

proof end;

end;

theorem Th21: :: TOPREAL1:21

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

proof end;

theorem Th22: :: 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 Th25: :: 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 c₁ be Nat;
let c₂ be FinSequence of (TOP-REAL c₁);
let c₃ be Nat;
func LSeg c₂,c₃ -> Subset of (TOP-REAL a₁) equals :Def5: :: TOPREAL1:def 5
LSeg (a₂ /. a₃),(a₂ /. (a₃ + 1)) if ( 1 <= a₃ & a₃ + 1 <= len a₂ )
otherwise {} ;
coherence

proof end;

correctness ;

end;

:: deftheorem Def5 defines LSeg TOPREAL1:def 5 :

theorem Th27: :: TOPREAL1:27

for b₁, b₂ being Nat
for b₃ being FinSequence of (TOP-REAL b₁) st 1 <= b₂ & b₂ + 1 <= len b₃ holds
( b₃ /. b₂ in LSeg b₃,b₂ & b₃ /. (b₂ + 1) in LSeg b₃,b₂ )

proof end;

definition

let c₁ be Nat;
let c₂ be FinSequence of (TOP-REAL c₁);
func L~ c₂ -> Subset of (TOP-REAL a₁) equals :: TOPREAL1:def 6
union { (LSeg a₂,b₁) where B is Nat : ( 1 <= b₁ & b₁ + 1 <= len a₂ ) } ;
coherence

proof end;

end;

:: deftheorem Def6 defines L~ TOPREAL1:def 6 :

theorem Th28: :: TOPREAL1:28

for b₁ being Nat
for b₂ being FinSequence of (TOP-REAL b₁) holds
( ( len b₂ = 0 or len b₂ = 1 ) iff L~ b₂ = {} )

proof end;

theorem Th29: :: TOPREAL1:29

for b₁ being Nat
for b₂ being FinSequence of (TOP-REAL b₁) st len b₂ >= 2 holds
L~ b₂ <> {}

proof end;

definition

let c₁ be FinSequence of (TOP-REAL 2);
attr a₁ is special means :: TOPREAL1:def 7
for b₁ being Nat st 1 <= b₁ & b₁ + 1 <= len a₁ & not (a₁ /. b₁) `1 = (a₁ /. (b₁ + 1)) `1 holds
(a₁ /. b₁) `2 = (a₁ /. (b₁ + 1)) `2 ;
attr a₁ is unfolded means :Def8: :: TOPREAL1:def 8
for b₁ being Nat st 1 <= b₁ & b₁ + 2 <= len a₁ holds
(LSeg a₁,b₁) /\ (LSeg a₁,(b₁ + 1)) = {(a₁ /. (b₁ + 1))};
attr a₁ is s.n.c. means :Def9: :: TOPREAL1:def 9
for b₁, b₂ being Nat st b₁ + 1 < b₂ holds
LSeg a₁,b₁ misses LSeg a₁,b₂;

end;

:: deftheorem Def7 defines special TOPREAL1:def 7 :

:: deftheorem Def8 defines unfolded TOPREAL1:def 8 :

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

definition

let c₁ be FinSequence of (TOP-REAL 2);
attr a₁ is being_S-Seq means :Def10: :: TOPREAL1:def 10
( a₁ is one-to-one & len a₁ >= 2 & a₁ is unfolded & a₁ is s.n.c. & a₁ is special );

end;

:: deftheorem Def10 defines being_S-Seq TOPREAL1:def 10 :

notation

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

end;

theorem Th30: :: TOPREAL1:30

ex b₁, b₂ being FinSequence of (TOP-REAL 2) st
( b₁ is_S-Seq & b₂ is_S-Seq & R^2-unit_square = (L~ b₁) \/ (L~ b₂) & (L~ b₁) /\ (L~ b₂) = {|[0,0]|,|[1,1]|} & b₁ /. 1 = |[0,0]| & b₁ /. (len b₁) = |[1,1]| & b₂ /. 1 = |[0,0]| & b₂ /. (len b₂) = |[1,1]| )

proof end;

theorem Th31: :: TOPREAL1:31

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

proof end;

definition

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

end;

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

notation

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

end;

theorem Th32: :: TOPREAL1:32

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

proof end;

registration

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

end;

theorem Th33: :: TOPREAL1:33

canceled;

theorem Th34: :: TOPREAL1:34

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

proof end;

theorem Th35: :: TOPREAL1:35

for b₁ being Subset of (TOP-REAL 2) st b₁ is_S-P_arc holds
ex b₂, b₃ being Point of (TOP-REAL 2) st b₁ is_an_arc_of b₂,b₃

proof end;

theorem Th36: :: TOPREAL1:36

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

proof end;