:: The Jordan's Property for Certain Subsets of the Plane
:: by Yatsuka Nakamura and Jaros{\l}aw Kotowicz
::
:: Received August 24, 1992
:: Copyright (c) 1992 Association of Mizar Users
Lm1:
( 0 in [.0 ,1.] & 1 in [.0 ,1.] )
theorem :: JORDAN1:1
canceled;
theorem :: JORDAN1:2
canceled;
theorem :: JORDAN1:3
canceled;
theorem Th4: :: JORDAN1:4
theorem Th5: :: JORDAN1:5
theorem :: JORDAN1:6
theorem Th7: :: JORDAN1:7
theorem Th8: :: JORDAN1:8
:: deftheorem defines convex JORDAN1:def 1 :
theorem Th9: :: JORDAN1:9
Lm2:
for s1 being Real holds { |[sb,tb]| where sb, tb is Real : sb < s1 } is Subset of (REAL 2)
Lm3:
for t1 being Real holds { |[sb,tb]| where sb, tb is Real : tb < t1 } is Subset of (REAL 2)
Lm4:
for s2 being Real holds { |[sb,tb]| where sb, tb is Real : s2 < sb } is Subset of (REAL 2)
Lm5:
for t2 being Real holds { |[sb,tb]| where sb, tb is Real : t2 < tb } is Subset of (REAL 2)
Lm6:
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)
Lm7:
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)
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 }
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 }
theorem Th14: :: JORDAN1:14
theorem :: JORDAN1:15
theorem Th16: :: JORDAN1:16
theorem :: JORDAN1:17
theorem Th18: :: JORDAN1:18
theorem :: JORDAN1:19
theorem Th20: :: JORDAN1:20
theorem :: JORDAN1:21
theorem Th22: :: JORDAN1:22
theorem :: JORDAN1:23
theorem Th24: :: JORDAN1:24
theorem Th25: :: JORDAN1:25
theorem Th26: :: JORDAN1:26
theorem Th27: :: JORDAN1:27
theorem Th28: :: JORDAN1:28
theorem Th29: :: JORDAN1:29
theorem Th30: :: JORDAN1:30
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
theorem Th32: :: JORDAN1:32
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 ) }
theorem Th34: :: JORDAN1:34
theorem Th35: :: JORDAN1:35
theorem Th36: :: JORDAN1:36
theorem Th37: :: JORDAN1:37
theorem Th38: :: JORDAN1:38
theorem Th39: :: JORDAN1:39
theorem Th40: :: JORDAN1:40
theorem Th41: :: JORDAN1:41
Lm8:
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
Lm9:
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
theorem Th42: :: JORDAN1:42
theorem Th43: :: JORDAN1:43
theorem :: JORDAN1:44
theorem Th45: :: JORDAN1:45
theorem :: JORDAN1:46
:: deftheorem Def2 defines Jordan JORDAN1:def 2 :
theorem :: JORDAN1:47
theorem :: JORDAN1:48
theorem :: JORDAN1:49
theorem :: JORDAN1:50
theorem Th51: :: JORDAN1:51
theorem :: JORDAN1:52
Lm10:
for x0, y0 being Real
for P being Subset of (TOP-REAL 2) st P = { |[x,y0]| where x is Real : x <= x0 } holds
P is convex
Lm11:
for x0, y0 being Real
for P being Subset of (TOP-REAL 2) st P = { |[x0,y]| where y is Real : y <= y0 } holds
P is convex
Lm12:
for x0, y0 being Real
for P being Subset of (TOP-REAL 2) st P = { |[x,y0]| where x is Real : x >= x0 } holds
P is convex
Lm13:
for x0, y0 being Real
for P being Subset of (TOP-REAL 2) st P = { |[x0,y]| where y is Real : y >= y0 } holds
P is convex