:: 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-2012 Association of Mizar Users begin Lm1: for r being real number 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 ) proofend; theorem Th1: :: JORDAN22:1 for C being Simple_closed_curve for i being Element of NAT holds (Upper_Appr C) . i c= Cl (RightComp (Cage (C,0))) proofend; theorem Th2: :: JORDAN22:2 for C being Simple_closed_curve for i being Element of NAT holds (Lower_Appr C) . i c= Cl (RightComp (Cage (C,0))) proofend; registration let C be Simple_closed_curve; cluster Upper_Arc C -> connected ; coherence Upper_Arc C is connected proofend; cluster Lower_Arc C -> connected ; coherence Lower_Arc C is connected proofend; end; theorem :: JORDAN22:3 for C being Simple_closed_curve for i being Element of NAT holds ( (Upper_Appr C) . i is compact & (Upper_Appr C) . i is connected ) proofend; theorem :: JORDAN22:4 for C being Simple_closed_curve for i being Element of NAT holds ( (Lower_Appr C) . i is compact & (Lower_Appr C) . i is connected ) proofend; registration let C be Simple_closed_curve; cluster North_Arc C -> compact ; coherence North_Arc C is compact proofend; cluster South_Arc C -> compact ; coherence South_Arc C is compact proofend; 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 Element of NAT holds 1 <= len (Gauge (R,n)) proofend; theorem Th5: :: JORDAN22:5 for R being non empty Subset of (TOP-REAL 2) for n being Element of NAT holds [1,1] in Indices (Gauge (R,n)) proofend; theorem Th6: :: JORDAN22:6 for R being non empty Subset of (TOP-REAL 2) for n being Element of NAT holds [1,2] in Indices (Gauge (R,n)) proofend; theorem Th7: :: JORDAN22:7 for R being non empty Subset of (TOP-REAL 2) for n being Element of NAT holds [2,1] in Indices (Gauge (R,n)) proofend; theorem Th8: :: JORDAN22:8 for i, m, k, j being Element of 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)))) proofend; theorem Th9: :: JORDAN22:9 for m, k being Element of 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))) proofend; theorem Th10: :: JORDAN22:10 for i, m, k, j being Element of 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))) proofend; theorem Th11: :: JORDAN22:11 for m, k being Element of 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))) proofend; theorem :: JORDAN22:12 for C being Simple_closed_curve for i being Element of NAT for r, t being real number st r > 0 & t > 0 holds ex n being Element of 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 ) proofend; theorem Th13: :: JORDAN22:13 for C being Simple_closed_curve for n being Element of 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)))) proofend; theorem Th14: :: JORDAN22:14 for C being Simple_closed_curve for n being Element of 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)))) proofend; theorem :: JORDAN22:15 for C being Simple_closed_curve for n being Element of 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 Element of 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 Element of NAT holds (UMP C) `2 < (UMP (L~ (Cage (C,n)))) `2 proofend; theorem Th18: :: JORDAN22:18 for C being Simple_closed_curve for n being Element of NAT holds (LMP C) `2 > (LMP (L~ (Cage (C,n)))) `2 proofend; theorem Th19: :: JORDAN22:19 for C being Simple_closed_curve for n being Element of NAT st 0 < n holds ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & UMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) ) proofend; theorem Th20: :: JORDAN22:20 for C being Simple_closed_curve for n being Element of NAT st 0 < n holds ex i being Element of NAT st ( 1 <= i & i <= len (Gauge (C,n)) & LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) ) proofend; theorem Th21: :: JORDAN22:21 for C being Simple_closed_curve for n being Element of NAT st 0 < n holds UMP (L~ (Cage (C,n))) = UMP (Upper_Arc (L~ (Cage (C,n)))) proofend; theorem Th22: :: JORDAN22:22 for C being Simple_closed_curve for n being Element of NAT st 0 < n holds LMP (L~ (Cage (C,n))) = LMP (Lower_Arc (L~ (Cage (C,n)))) proofend; theorem Th23: :: JORDAN22:23 for C being Simple_closed_curve for n being Element of NAT st 0 < n holds (UMP C) `2 < (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 proofend; theorem Th24: :: JORDAN22:24 for C being Simple_closed_curve for n being Element of NAT st 0 < n holds (LMP (Lower_Arc (L~ (Cage (C,n))))) `2 < (LMP C) `2 proofend; theorem Th25: :: JORDAN22:25 for C being Simple_closed_curve for i, j being Element of NAT st i <= j holds (UMP (L~ (Cage (C,j)))) `2 <= (UMP (L~ (Cage (C,i)))) `2 proofend; theorem Th26: :: JORDAN22:26 for C being Simple_closed_curve for i, j being Element of NAT st i <= j holds (LMP (L~ (Cage (C,i)))) `2 <= (LMP (L~ (Cage (C,j)))) `2 proofend; theorem Th27: :: JORDAN22:27 for C being Simple_closed_curve for i, j being Element of NAT st 0 < i & i <= j holds (UMP (Upper_Arc (L~ (Cage (C,j))))) `2 <= (UMP (Upper_Arc (L~ (Cage (C,i))))) `2 proofend; theorem Th28: :: JORDAN22:28 for C being Simple_closed_curve for i, j being Element of NAT st 0 < i & i <= j holds (LMP (Lower_Arc (L~ (Cage (C,i))))) `2 <= (LMP (Lower_Arc (L~ (Cage (C,j))))) `2 proofend; begin theorem Th29: :: JORDAN22:29 for C being Simple_closed_curve holds W-min C in North_Arc C proofend; theorem Th30: :: JORDAN22:30 for C being Simple_closed_curve holds E-max C in North_Arc C proofend; theorem Th31: :: JORDAN22:31 for C being Simple_closed_curve holds W-min C in South_Arc C proofend; theorem Th32: :: JORDAN22:32 for C being Simple_closed_curve holds E-max C in South_Arc C proofend; 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 proofend; theorem Th34: :: JORDAN22:34 for C being Simple_closed_curve holds LMP C in South_Arc C proofend; theorem Th35: :: JORDAN22:35 for C being Simple_closed_curve holds North_Arc C c= C proofend; theorem Th36: :: JORDAN22:36 for C being Simple_closed_curve holds South_Arc C c= C proofend; 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 ) ) proofend; :: 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) proofend; theorem :: JORDAN22:39 for C being Simple_closed_curve holds E-bound C = E-bound (North_Arc C) proofend; theorem :: JORDAN22:40 for C being Simple_closed_curve holds W-bound C = W-bound (South_Arc C) proofend; theorem :: JORDAN22:41 for C being Simple_closed_curve holds E-bound C = E-bound (South_Arc C) proofend;