:: JORDAN1 semantic presentation

theorem Th1: :: JORDAN1:1

for GX being TopStruct
for A being Subset of GX holds the carrier of (GX | A) = A

proof end;

theorem Th2: :: JORDAN1:2

for GX being non empty TopSpace st ( for x, y being Point of GX ex GY being non empty TopSpace st
( GY is connected & ex f being Function of GY,GX st
( f is continuous & x in rng f & y in rng f ) ) ) holds
GX is connected

proof end;

Lm1: ( 0 in [.0,1.] & 1 in [.0,1.] )

proof end;

theorem :: JORDAN1:3

canceled;

theorem Th4: :: JORDAN1:4

for GX being non empty TopSpace st ( for x, y being Point of GX ex h being Function of I[01] ,GX st
( h is continuous & x = h . 0 & y = h . 1 ) ) holds
GX is connected

proof end;

theorem Th5: :: JORDAN1:5

for GX being non empty TopSpace
for A being Subset of GX st ( for xa, ya being Point of GX st xa in A & ya in A & xa <> ya holds
ex h being Function of I[01] ,(GX | A) st
( h is continuous & xa = h . 0 & ya = h . 1 ) ) holds
A is connected

proof end;

theorem Th6: :: JORDAN1:6

for GX being non empty TopSpace
for A0, A1 being Subset of GX st A0 is connected & A1 is connected & A0 meets A1 holds
A0 \/ A1 is connected

proof end;

theorem Th7: :: JORDAN1:7

for GX being non empty TopSpace
for A0, A1, A2 being Subset of GX st A0 is connected & A1 is connected & A2 is connected & A0 meets A1 & A1 meets A2 holds
(A0 \/ A1) \/ A2 is connected

proof end;

theorem Th8: :: JORDAN1:8

for GX being non empty TopSpace
for A0, A1, A2, A3 being Subset of GX st A0 is connected & A1 is connected & A2 is connected & A3 is connected & A0 meets A1 & A1 meets A2 & A2 meets A3 holds
((A0 \/ A1) \/ A2) \/ A3 is connected

proof end;

definition

let n be Nat;
let P be Subset of (TOP-REAL n);
attr P is convex means :: JORDAN1:def 1
for w1, w2 being Point of (TOP-REAL n) st w1 in P & w2 in P holds
LSeg w1,w2 c= P;

end;

:: deftheorem defines convex JORDAN1:def 1 :

theorem Th9: :: JORDAN1:9

for n being Nat
for P being Subset of (TOP-REAL n) st P is convex holds
P is connected

proof end;

Lm2: the carrier of (TOP-REAL 2) = REAL 2
by EUCLID:25;

Lm3: for s1 being Real holds { |[sb,tb]| where sb, tb is Real : sb < s1 } is Subset of (REAL 2)

proof end;

Lm4: for t1 being Real holds { |[sb,tb]| where sb, tb is Real : tb < t1 } is Subset of (REAL 2)

proof end;

Lm5: for s2 being Real holds { |[sb,tb]| where sb, tb is Real : s2 < sb } is Subset of (REAL 2)

proof end;

Lm6: for t2 being Real holds { |[sb,tb]| where sb, tb is Real : t2 < tb } is Subset of (REAL 2)

proof end;

Lm7: for s1, s2, t1, t2 being Real holds { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } is Subset of (REAL 2)

proof end;

Lm8: for s1, s2, t1, t2 being Real holds { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } is Subset of (REAL 2)

proof end;

theorem :: JORDAN1:10

canceled;

theorem :: JORDAN1:11

canceled;

theorem Th12: :: JORDAN1:12

for s1, s2, t1, t2 being Real holds { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } = (({ |[s3,t3]| where s3, t3 is Real : s1 < s3 } /\ { |[s4,t4]| where s4, t4 is Real : s4 < s2 } ) /\ { |[s5,t5]| where s5, t5 is Real : t1 < t5 } ) /\ { |[s6,t6]| where s6, t6 is Real : t6 < t2 }

proof end;

theorem Th13: :: JORDAN1:13

for s1, s2, t1, t2 being Real holds { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } = (({ |[s3,t3]| where s3, t3 is Real : s3 < s1 } \/ { |[s4,t4]| where s4, t4 is Real : t4 < t1 } ) \/ { |[s5,t5]| where s5, t5 is Real : s2 < s5 } ) \/ { |[s6,t6]| where s6, t6 is Real : t2 < t6 }

proof end;

theorem Th14: :: JORDAN1:14

for s1, t1, s2, t2 being Real
for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } holds
P is convex

proof end;

theorem Th15: :: JORDAN1:15

for s1, t1, s2, t2 being Real
for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } holds
P is connected

proof end;

theorem Th16: :: JORDAN1:16

for s1 being Real
for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : s1 < s } holds
P is convex

proof end;

theorem Th17: :: JORDAN1:17

for s1 being Real
for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : s1 < s } holds
P is connected

proof end;

theorem Th18: :: JORDAN1:18

for s2 being Real
for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : s < s2 } holds
P is convex

proof end;

theorem Th19: :: JORDAN1:19

for s2 being Real
for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : s < s2 } holds
P is connected

proof end;

theorem Th20: :: JORDAN1:20

for t1 being Real
for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : t1 < t } holds
P is convex

proof end;

theorem Th21: :: JORDAN1:21

for t1 being Real
for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : t1 < t } holds
P is connected

proof end;

theorem Th22: :: JORDAN1:22

for t2 being Real
for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : t < t2 } holds
P is convex

proof end;

theorem Th23: :: JORDAN1:23

for t2 being Real
for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : t < t2 } holds
P is connected

proof end;

theorem Th24: :: JORDAN1:24

for s1, t1, s2, t2 being Real
for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } holds
P is connected

proof end;

Lm9: for r, s being Real holds (s - r) ^2 = (r - s) ^2

proof end;

Lm10: TOP-REAL 2 = TopSpaceMetr (Euclid 2)
by EUCLID:def 8;

theorem Th25: :: JORDAN1:25

for s1 being Real
for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : s1 < s } holds
P is open

proof end;

theorem Th26: :: JORDAN1:26

for s1 being Real
for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : s1 > s } holds
P is open

proof end;

theorem Th27: :: JORDAN1:27

for s1 being Real
for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : s1 < t } holds
P is open

proof end;

theorem Th28: :: JORDAN1:28

for s1 being Real
for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : s1 > t } holds
P is open

proof end;

theorem Th29: :: JORDAN1:29

for s1, t1, s2, t2 being Real
for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } holds
P is open

proof end;

theorem Th30: :: JORDAN1:30

for s1, t1, s2, t2 being Real
for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } holds
P is open

proof end;

theorem Th31: :: JORDAN1:31

for s1, t1, s2, t2 being Real
for P, Q being Subset of (TOP-REAL 2) st P = { |[sa,ta]| where sa, ta is Real : ( s1 < sa & sa < s2 & t1 < ta & ta < t2 ) } & Q = { |[sb,tb]| where sb, tb is Real : ( not s1 <= sb or not sb <= s2 or not t1 <= tb or not tb <= t2 ) } holds
P misses Q

proof end;

theorem Th32: :: JORDAN1:32

for s1, s2, t1, t2 being Real holds { p where p is Point of (TOP-REAL 2) : ( s1 < p `1 & p `1 < s2 & t1 < p `2 & p `2 < t2 ) } = { |[sa,ta]| where sa, ta is Real : ( s1 < sa & sa < s2 & t1 < ta & ta < t2 ) }

proof end;

theorem Th33: :: JORDAN1:33

for s1, s2, t1, t2 being Real holds { qc where qc is Point of (TOP-REAL 2) : ( not s1 <= qc `1 or not qc `1 <= s2 or not t1 <= qc `2 or not qc `2 <= t2 ) } = { |[sb,tb]| where sb, tb is Real : ( not s1 <= sb or not sb <= s2 or not t1 <= tb or not tb <= t2 ) }

proof end;

theorem Th34: :: JORDAN1:34

for s1, s2, t1, t2 being Real holds { p0 where p0 is Point of (TOP-REAL 2) : ( s1 < p0 `1 & p0 `1 < s2 & t1 < p0 `2 & p0 `2 < t2 ) } is Subset of (TOP-REAL 2)

proof end;

theorem Th35: :: JORDAN1:35

for s1, s2, t1, t2 being Real holds { pq where pq is Point of (TOP-REAL 2) : ( not s1 <= pq `1 or not pq `1 <= s2 or not t1 <= pq `2 or not pq `2 <= t2 ) } is Subset of (TOP-REAL 2)

proof end;

theorem Th36: :: JORDAN1:36

for s1, t1, s2, t2 being Real
for P being Subset of (TOP-REAL 2) st P = { p0 where p0 is Point of (TOP-REAL 2) : ( s1 < p0 `1 & p0 `1 < s2 & t1 < p0 `2 & p0 `2 < t2 ) } holds
P is connected

proof end;

theorem Th37: :: JORDAN1:37

for s1, t1, s2, t2 being Real
for P being Subset of (TOP-REAL 2) st P = { pq where pq is Point of (TOP-REAL 2) : ( not s1 <= pq `1 or not pq `1 <= s2 or not t1 <= pq `2 or not pq `2 <= t2 ) } holds
P is connected

proof end;

theorem Th38: :: JORDAN1:38

for s1, t1, s2, t2 being Real
for P being Subset of (TOP-REAL 2) st P = { p0 where p0 is Point of (TOP-REAL 2) : ( s1 < p0 `1 & p0 `1 < s2 & t1 < p0 `2 & p0 `2 < t2 ) } holds
P is open

proof end;

theorem Th39: :: JORDAN1:39

for s1, t1, s2, t2 being Real
for P being Subset of (TOP-REAL 2) st P = { pq where pq is Point of (TOP-REAL 2) : ( not s1 <= pq `1 or not pq `1 <= s2 or not t1 <= pq `2 or not pq `2 <= t2 ) } holds
P is open

proof end;

theorem Th40: :: JORDAN1:40

for s1, t1, s2, t2 being Real
for P, Q being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : ( s1 < p `1 & p `1 < s2 & t1 < p `2 & p `2 < t2 ) } & Q = { qc where qc is Point of (TOP-REAL 2) : ( not s1 <= qc `1 or not qc `1 <= s2 or not t1 <= qc `2 or not qc `2 <= t2 ) } holds
P misses Q

proof end;

theorem Th41: :: JORDAN1:41

for s1, t1, s2, t2 being Real
for P, P1, P2 being Subset of (TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } & P1 = { pa where pa is Point of (TOP-REAL 2) : ( s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) } & P2 = { pb where pb is Point of (TOP-REAL 2) : ( not s1 <= pb `1 or not pb `1 <= s2 or not t1 <= pb `2 or not pb `2 <= t2 ) } holds
( P ` = P1 \/ P2 & P ` <> {} & P1 misses P2 & ( for P1A, P2B being Subset of ((TOP-REAL 2) | (P ` )) st P1A = P1 & P2B = P2 holds
( P1A is_a_component_of (TOP-REAL 2) | (P ` ) & P2B is_a_component_of (TOP-REAL 2) | (P ` ) ) ) )

proof end;

Lm11: for s1, t1, s2, t2 being Real
for P, P1 being Subset of (TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } & P1 = { pa where pa is Point of (TOP-REAL 2) : ( s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) } holds
Cl P1 = P \/ P1

proof end;

Lm12: for s1, t1, s2, t2 being Real
for P, P2 being Subset of (TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } & P2 = { pb where pb is Point of (TOP-REAL 2) : ( not s1 <= pb `1 or not pb `1 <= s2 or not t1 <= pb `2 or not pb `2 <= t2 ) } holds
Cl P2 = P \/ P2

proof end;

theorem Th42: :: JORDAN1:42

proof end;

theorem Th43: :: JORDAN1:43

for s1, s2, t1, t2 being Real
for P, P1 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } & P1 = { pa where pa is Point of (TOP-REAL 2) : ( s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) } holds
P1 c= [#] ((TOP-REAL 2) | (P ` ))

proof end;

theorem :: JORDAN1:44

proof end;

theorem Th45: :: JORDAN1:45

for s1, s2, t1, t2 being Real
for P, P2 being Subset of (TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } & P2 = { pb where pb is Point of (TOP-REAL 2) : ( not s1 <= pb `1 or not pb `1 <= s2 or not t1 <= pb `2 or not pb `2 <= t2 ) } holds
P2 c= [#] ((TOP-REAL 2) | (P ` ))

proof end;

theorem :: JORDAN1:46

proof end;

definition

let S be Subset of (TOP-REAL 2);
attr S is Jordan means :Def2: :: JORDAN1:def 2
( S ` <> {} & ex A1, A2 being Subset of (TOP-REAL 2) st
( S ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & ( for C1, C2 being Subset of ((TOP-REAL 2) | (S ` )) st C1 = A1 & C2 = A2 holds
( C1 is_a_component_of (TOP-REAL 2) | (S ` ) & C2 is_a_component_of (TOP-REAL 2) | (S ` ) ) ) ) );

end;

:: deftheorem Def2 defines Jordan JORDAN1:def 2 :

notation

let S be Subset of (TOP-REAL 2);
synonym S has_property_J for Jordan S;

end;

theorem :: JORDAN1:47

for S being Subset of (TOP-REAL 2) st S has_property_J holds
( S ` <> {} & ex A1, A2 being Subset of (TOP-REAL 2) ex C1, C2 being Subset of ((TOP-REAL 2) | (S ` )) st
( S ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & C1 = A1 & C2 = A2 & C1 is_a_component_of (TOP-REAL 2) | (S ` ) & C2 is_a_component_of (TOP-REAL 2) | (S ` ) & ( for C3 being Subset of ((TOP-REAL 2) | (S ` )) holds
( not C3 is_a_component_of (TOP-REAL 2) | (S ` ) or C3 = C1 or C3 = C2 ) ) ) )

proof end;

theorem :: JORDAN1:48

for s1, s2, t1, t2 being Real
for P being Subset of (TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } holds
P has_property_J

proof end;

theorem :: JORDAN1:49

for s1, t1, s2, t2 being Real
for P, P2 being Subset of (TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } & P2 = { pb where pb is Point of (TOP-REAL 2) : ( not s1 <= pb `1 or not pb `1 <= s2 or not t1 <= pb `2 or not pb `2 <= t2 ) } holds
Cl P2 = P \/ P2 by Lm12;

theorem :: JORDAN1:50

for s1, t1, s2, t2 being Real
for P, P1 being Subset of (TOP-REAL 2) st s1 < s2 & t1 < t2 & P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } & P1 = { pa where pa is Point of (TOP-REAL 2) : ( s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) } holds
Cl P1 = P \/ P1 by Lm11;