:: by Artur Korni{\l}owicz and Adam Grabowski

::

:: Received October 6, 2004

:: Copyright (c) 2004-2019 Association of Mizar Users

Lm1: for r being Real

for X being Subset of (TOP-REAL 2) st r in proj2 .: X holds

ex x being Point of (TOP-REAL 2) st

( x in X & proj2 . x = r )

proof end;

theorem Th1: :: JORDAN22:1

for C being Simple_closed_curve

for i being Nat holds (Upper_Appr C) . i c= Cl (RightComp (Cage (C,0)))

for i being Nat holds (Upper_Appr C) . i c= Cl (RightComp (Cage (C,0)))

proof end;

theorem Th2: :: JORDAN22:2

for C being Simple_closed_curve

for i being Nat holds (Lower_Appr C) . i c= Cl (RightComp (Cage (C,0)))

for i being Nat holds (Lower_Appr C) . i c= Cl (RightComp (Cage (C,0)))

proof end;

registration

let C be Simple_closed_curve;

coherence

Upper_Arc C is connected

Lower_Arc C is connected

end;
coherence

Upper_Arc C is connected

proof end;

coherence Lower_Arc C is connected

proof end;

theorem :: JORDAN22:3

for C being Simple_closed_curve

for i being Nat holds

( (Upper_Appr C) . i is compact & (Upper_Appr C) . i is connected )

for i being Nat holds

( (Upper_Appr C) . i is compact & (Upper_Appr C) . i is connected )

proof end;

theorem :: JORDAN22:4

for C being Simple_closed_curve

for i being Nat holds

( (Lower_Appr C) . i is compact & (Lower_Appr C) . i is connected )

for i being Nat holds

( (Lower_Appr C) . i is compact & (Lower_Appr C) . i is connected )

proof end;

registration

let C be Simple_closed_curve;

coherence

North_Arc C is compact

South_Arc C is compact

end;
coherence

North_Arc C is compact

proof end;

coherence South_Arc C is compact

proof end;

Lm2: dom proj2 = the carrier of (TOP-REAL 2)

by FUNCT_2:def 1;

Lm3: for R being non empty Subset of (TOP-REAL 2)

for n being Nat holds 1 <= len (Gauge (R,n))

proof end;

theorem Th8: :: JORDAN22:8

for i, j, k, m being Nat

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k & [i,j] in Indices (Gauge (C,k)) & [i,(j + 1)] in Indices (Gauge (C,k)) holds

dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * (i,(j + 1))))

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k & [i,j] in Indices (Gauge (C,k)) & [i,(j + 1)] in Indices (Gauge (C,k)) holds

dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * (i,(j + 1)))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * (i,(j + 1))))

proof end;

theorem Th9: :: JORDAN22:9

for k, m being Nat

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k holds

dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2)))

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k holds

dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (1,2))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (1,2)))

proof end;

theorem Th10: :: JORDAN22:10

for i, j, k, m being Nat

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k & [i,j] in Indices (Gauge (C,k)) & [(i + 1),j] in Indices (Gauge (C,k)) holds

dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * ((i + 1),j))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * ((i + 1),j)))

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k & [i,j] in Indices (Gauge (C,k)) & [(i + 1),j] in Indices (Gauge (C,k)) holds

dist (((Gauge (C,m)) * (i,j)),((Gauge (C,m)) * ((i + 1),j))) < dist (((Gauge (C,k)) * (i,j)),((Gauge (C,k)) * ((i + 1),j)))

proof end;

theorem Th11: :: JORDAN22:11

for k, m being Nat

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k holds

dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1)))

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k holds

dist (((Gauge (C,m)) * (1,1)),((Gauge (C,m)) * (2,1))) < dist (((Gauge (C,k)) * (1,1)),((Gauge (C,k)) * (2,1)))

proof end;

theorem :: JORDAN22:12

for C being Simple_closed_curve

for i being Nat

for r, t being Real st r > 0 & t > 0 holds

ex n being Nat st

( i < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t )

for i being Nat

for r, t being Real st r > 0 & t > 0 holds

ex n being Nat st

( i < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t )

proof end;

theorem Th13: :: JORDAN22:13

for C being Simple_closed_curve

for n being Nat st 0 < n holds

upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))

for n being Nat st 0 < n holds

upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))

proof end;

theorem Th14: :: JORDAN22:14

for C being Simple_closed_curve

for n being Nat st 0 < n holds

lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))

for n being Nat st 0 < n holds

lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))) = lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (Vertical_Line (((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2))))

proof end;

theorem :: JORDAN22:15

for C being Simple_closed_curve

for n being Nat st 0 < n holds

UMP (L~ (Cage (C,n))) = |[(((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2),(upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))))]| by Th13;

for n being Nat st 0 < n holds

UMP (L~ (Cage (C,n))) = |[(((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2),(upper_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))))]| by Th13;

theorem :: JORDAN22:16

for C being Simple_closed_curve

for n being Nat st 0 < n holds

LMP (L~ (Cage (C,n))) = |[(((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2),(lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))))]| by Th14;

for n being Nat st 0 < n holds

LMP (L~ (Cage (C,n))) = |[(((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2),(lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))))]| by Th14;

theorem Th19: :: JORDAN22:19

for C being Simple_closed_curve

for n being Nat st 0 < n holds

ex i being Nat st

( 1 <= i & i <= len (Gauge (C,n)) & UMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) )

for n being Nat st 0 < n holds

ex i being Nat st

( 1 <= i & i <= len (Gauge (C,n)) & UMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) )

proof end;

theorem Th20: :: JORDAN22:20

for C being Simple_closed_curve

for n being Nat st 0 < n holds

ex i being Nat st

( 1 <= i & i <= len (Gauge (C,n)) & LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) )

for n being Nat st 0 < n holds

ex i being Nat st

( 1 <= i & i <= len (Gauge (C,n)) & LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) )

proof end;

theorem Th21: :: JORDAN22:21

for C being Simple_closed_curve

for n being Nat st 0 < n holds

UMP (L~ (Cage (C,n))) = UMP (Upper_Arc (L~ (Cage (C,n))))

for n being Nat st 0 < n holds

UMP (L~ (Cage (C,n))) = UMP (Upper_Arc (L~ (Cage (C,n))))

proof end;

theorem Th22: :: JORDAN22:22

for C being Simple_closed_curve

for n being Nat st 0 < n holds

LMP (L~ (Cage (C,n))) = LMP (Lower_Arc (L~ (Cage (C,n))))

for n being Nat st 0 < n holds

LMP (L~ (Cage (C,n))) = LMP (Lower_Arc (L~ (Cage (C,n))))

proof end;

theorem Th23: :: JORDAN22:23

for C being Simple_closed_curve

for n being Nat st 0 < n holds

(UMP C) `2 < (UMP (Upper_Arc (L~ (Cage (C,n))))) `2

for n being Nat st 0 < n holds

(UMP C) `2 < (UMP (Upper_Arc (L~ (Cage (C,n))))) `2

proof end;

theorem Th24: :: JORDAN22:24

for C being Simple_closed_curve

for n being Nat st 0 < n holds

(LMP (Lower_Arc (L~ (Cage (C,n))))) `2 < (LMP C) `2

for n being Nat st 0 < n holds

(LMP (Lower_Arc (L~ (Cage (C,n))))) `2 < (LMP C) `2

proof end;

theorem Th25: :: JORDAN22:25

for C being Simple_closed_curve

for i, j being Nat st i <= j holds

(UMP (L~ (Cage (C,j)))) `2 <= (UMP (L~ (Cage (C,i)))) `2

for i, j being Nat st i <= j holds

(UMP (L~ (Cage (C,j)))) `2 <= (UMP (L~ (Cage (C,i)))) `2

proof end;

theorem Th26: :: JORDAN22:26

for C being Simple_closed_curve

for i, j being Nat st i <= j holds

(LMP (L~ (Cage (C,i)))) `2 <= (LMP (L~ (Cage (C,j)))) `2

for i, j being Nat st i <= j holds

(LMP (L~ (Cage (C,i)))) `2 <= (LMP (L~ (Cage (C,j)))) `2

proof end;

theorem Th27: :: JORDAN22:27

for C being Simple_closed_curve

for i, j being Nat st 0 < i & i <= j holds

(UMP (Upper_Arc (L~ (Cage (C,j))))) `2 <= (UMP (Upper_Arc (L~ (Cage (C,i))))) `2

for i, j being Nat st 0 < i & i <= j holds

(UMP (Upper_Arc (L~ (Cage (C,j))))) `2 <= (UMP (Upper_Arc (L~ (Cage (C,i))))) `2

proof end;

theorem Th28: :: JORDAN22:28

for C being Simple_closed_curve

for i, j being Nat st 0 < i & i <= j holds

(LMP (Lower_Arc (L~ (Cage (C,i))))) `2 <= (LMP (Lower_Arc (L~ (Cage (C,j))))) `2

for i, j being Nat st 0 < i & i <= j holds

(LMP (Lower_Arc (L~ (Cage (C,i))))) `2 <= (LMP (Lower_Arc (L~ (Cage (C,j))))) `2

proof end;

Lm4: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2)

by EUCLID:def 8;

theorem :: JORDAN22:37

for C being Simple_closed_curve holds

( ( LMP C in Lower_Arc C & UMP C in Upper_Arc C ) or ( UMP C in Lower_Arc C & LMP C in Upper_Arc C ) )

( ( LMP C in Lower_Arc C & UMP C in Upper_Arc C ) or ( UMP C in Lower_Arc C & LMP C in Upper_Arc C ) )

proof end;

:: Moved from JORDAN, AG 20.01.2006