:: On Some Points of a Simple Closed Curve. {P}art {II}
:: by Artur Korni{\l}owicz and Adam Grabowski
::
:: Received October 6, 2004
:: Copyright (c) 2004-2016 Association of Mizar Users

environ

vocabularies HIDDEN, NUMBERS, TOPREAL2, SUBSET_1, EUCLID, RELAT_1, PRE_TOPC, FUNCT_1, STRUCT_0, JORDAN19, TARSKI, GOBOARD9, JORDAN9, CARD_1, JORDAN6, TOPREAL1, RELAT_2, PSCOMP_1, RCOMP_1, KURATO_2, XBOOLE_0, XXREAL_0, FINSEQ_1, JORDAN8, MATRIX_1, TREES_1, SPPOL_1, ARYTM_3, METRIC_1, ARYTM_1, NEWTON, ORDINAL2, RLTOPSP1, JORDAN1A, MCART_1, XXREAL_2, SEQ_4, GOBOARD2, JORDAN21, JORDAN2C, GOBOARD1, FINSEQ_6, GOBOARD5, PARTFUN1, PCOMPS_1, WEIERSTR, SEQ_1, SEQ_2, REAL_1, COMPLEX1, JORDAN10, JORDAN3, CONVEX1, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, COMPLEX1, NAT_1, NAT_D, RELSET_1, PARTFUN1, FUNCT_2, XXREAL_2, SEQ_4, NEWTON, FINSEQ_1, MATRIX_0, DOMAIN_1, STRUCT_0, PRE_TOPC, COMPTS_1, FINSEQ_6, CONNSP_1, METRIC_1, PCOMPS_1, PSCOMP_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, GOBOARD1, GOBOARD2, WEIERSTR, SPPOL_1, GOBOARD5, TOPRNS_1, JORDAN2C, JORDAN6, GOBOARD9, JORDAN8, JORDAN9, GOBRD13, TOPREAL6, JORDAN10, JORDAN1K, JORDAN1A, KURATO_2, JORDAN19, JORDAN21;
definitions TARSKI, TOPRNS_1, XXREAL_2;
theorems XBOOLE_1, JORDAN1A, JORDAN6, XBOOLE_0, JORDAN1K, EUCLID, TOPREAL1, TARSKI, JORDAN16, METRIC_1, SPRECT_3, TOPMETR, JORDAN7, GOBRD14, JORDAN1I, INT_1, GOBOARD5, FINSEQ_6, REVROT_1, SPRECT_2, GOBOARD7, JGRAPH_1, JORDAN1H, JORDAN9, GOBRD13, NAT_1, JORDAN8, SUBSET_1, JORDAN2C, JORDAN10, PSCOMP_1, SPPOL_2, SPPOL_1, SEQ_4, FUNCT_2, WEIERSTR, JORDAN1G, TOPRNS_1, ABSVALUE, JORDAN19, KURATO_2, JORDAN21, XREAL_1, JORDAN1J, JORDAN1B, RELAT_1, JORDAN5D, TOPREAL3, JORDAN1F, NEWTON, SPRECT_1, XXREAL_0, PEPIN, TOPREAL6, JCT_MISC, MATRIX_0, XXREAL_2, NAT_D, XREAL_0, COMPTS_1, PRE_TOPC, RLTOPSP1, ORDINAL1;
schemes FUNCT_2;
registrations XBOOLE_0, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_6, STRUCT_0, COMPTS_1, EUCLID, TOPREAL1, TOPREAL2, GOBOARD2, SPPOL_2, TOPREAL5, SPRECT_2, JORDAN6, SPRECT_3, JORDAN2C, REVROT_1, TOPREAL6, JORDAN21, JORDAN8, JORDAN10, VALUED_0, FUNCT_1, ORDINAL1, RLTOPSP1, JORDAN1, XCMPLX_0, NEWTON;
constructors HIDDEN, REAL_1, RCOMP_1, NEWTON, BINARITH, CONNSP_1, MONOID_0, TOPRNS_1, TOPREAL4, GOBOARD2, PSCOMP_1, GOBOARD9, JORDAN5C, JORDAN6, JORDAN2C, TOPREAL6, JORDAN1K, JORDAN21, JORDAN8, GOBRD13, JORDAN9, JORDAN10, JORDAN1A, KURATO_2, JORDAN19, NAT_D, SEQ_4, FUNCSDOM, CONVEX1, JORDAN11;
requirements HIDDEN, SUBSET, BOOLE, REAL, NUMERALS, ARITHM;
equalities JORDAN6, JORDAN21;
expansions TARSKI, JORDAN6, XXREAL_2;


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

registration
let C be Simple_closed_curve;
cluster Upper_Arc C -> connected ;
coherence
Upper_Arc C is connected
proof end;
cluster Lower_Arc C -> connected ;
coherence
Lower_Arc C is connected
proof end;
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 )
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 )
proof end;

registration
let C be Simple_closed_curve;
cluster North_Arc C -> compact ;
coherence
North_Arc C is compact
proof end;
cluster South_Arc C -> compact ;
coherence
South_Arc C is compact
proof end;
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 Th5: :: JORDAN22:5
for R being non empty Subset of (TOP-REAL 2)
for n being Nat holds [1,1] in Indices (Gauge (R,n))
proof end;

theorem Th6: :: JORDAN22:6
for R being non empty Subset of (TOP-REAL 2)
for n being Nat holds [1,2] in Indices (Gauge (R,n))
proof end;

theorem Th7: :: JORDAN22:7
for R being non empty Subset of (TOP-REAL 2)
for n being Nat holds [2,1] in Indices (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))))
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)))
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)))
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)))
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 )
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))))
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))))
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;

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;

theorem Th17: :: JORDAN22:17
for C being Simple_closed_curve
for n being Nat holds (UMP C) `2 < (UMP (L~ (Cage (C,n)))) `2
proof end;

theorem Th18: :: JORDAN22:18
for C being Simple_closed_curve
for n being Nat holds (LMP C) `2 > (LMP (L~ (Cage (C,n)))) `2
proof end;

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

theorem Th29: :: JORDAN22:29
for C being Simple_closed_curve holds W-min C in North_Arc C
proof end;

theorem Th30: :: JORDAN22:30
for C being Simple_closed_curve holds E-max C in North_Arc C
proof end;

theorem Th31: :: JORDAN22:31
for C being Simple_closed_curve holds W-min C in South_Arc C
proof end;

theorem Th32: :: JORDAN22:32
for C being Simple_closed_curve holds E-max C in South_Arc C
proof end;

Lm4: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2)
by EUCLID:def 8;

theorem Th33: :: JORDAN22:33
for C being Simple_closed_curve holds UMP C in North_Arc C
proof end;

theorem Th34: :: JORDAN22:34
for C being Simple_closed_curve holds LMP C in South_Arc C
proof end;

theorem Th35: :: JORDAN22:35
for C being Simple_closed_curve holds North_Arc C c= C
proof end;

theorem Th36: :: JORDAN22:36
for C being Simple_closed_curve holds South_Arc C c= C
proof end;

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

:: Moved from JORDAN, AG 20.01.2006
theorem :: JORDAN22:38
for C being Simple_closed_curve holds W-bound C = W-bound (North_Arc C)
proof end;

theorem :: JORDAN22:39
for C being Simple_closed_curve holds E-bound C = E-bound (North_Arc C)
proof end;

theorem :: JORDAN22:40
for C being Simple_closed_curve holds W-bound C = W-bound (South_Arc C)
proof end;

theorem :: JORDAN22:41
for C being Simple_closed_curve holds E-bound C = E-bound (South_Arc C)
proof end;