:: Some Properties of Cells and Gauges :: by Adam Grabowski , Artur Korni{\l}owicz and Andrzej Trybulec :: :: Received October 13, 2000 :: Copyright (c) 2000-2012 Association of Mizar Users begin Lm1: now__::_thesis:_for_r_being_real_number_ for_j_being_Element_of_NAT_holds_[\(r_+_j)/]_-_j_=_[\r/] let r be real number ; ::_thesis: for j being Element of NAT holds [\(r + j)/] - j = [\r/] let j be Element of NAT ; ::_thesis: [\(r + j)/] - j = [\r/] thus [\(r + j)/] - j = ([\r/] + j) - j by INT_1:28 .= [\r/] ; ::_thesis: verum end; Lm2: for a, b, c being real number st a <> 0 & b <> 0 holds (a / b) * ((c / a) * b) = c proofend; Lm3: for p being Point of (TOP-REAL 2) holds p is Point of (Euclid 2) proofend; Lm4: for r being real number st r > 0 holds 2 * (r / 4) < r proofend; theorem Th1: :: JORDAN1C:1 for C being Simple_closed_curve for i, j, n being Element of NAT st [i,j] in Indices (Gauge (C,n)) & [(i + 1),j] in Indices (Gauge (C,n)) holds dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) = (((Gauge (C,n)) * ((i + 1),j)) `1) - (((Gauge (C,n)) * (i,j)) `1) proofend; theorem Th2: :: JORDAN1C:2 for C being Simple_closed_curve for i, j, n being Element of NAT st [i,j] in Indices (Gauge (C,n)) & [i,(j + 1)] in Indices (Gauge (C,n)) holds dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) = (((Gauge (C,n)) * (i,(j + 1))) `2) - (((Gauge (C,n)) * (i,j)) `2) proofend; TopSpaceMetr (Euclid 2) = TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) by EUCLID:def_8; then Lm5: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopStruct(# the carrier of (Euclid 2),(Family_open_set (Euclid 2)) #) by PCOMPS_1:def_5; Lm6: for C being Simple_closed_curve for i, n, j being Element of NAT for p being Point of (TOP-REAL 2) for r being real number for q being Point of (Euclid 2) st 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) & r > 0 & p = q & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r / 4 & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < r / 4 & p in cell ((Gauge (C,n)),i,j) holds cell ((Gauge (C,n)),i,j) c= Ball (q,r) proofend; theorem Th3: :: JORDAN1C:3 for S being Subset of (TOP-REAL 2) st S is bounded holds proj1 .: S is real-bounded proofend; theorem :: JORDAN1C:4 for C1 being non empty compact Subset of (TOP-REAL 2) for C2, S being non empty Subset of (TOP-REAL 2) st S = C1 \/ C2 & not proj1 .: C2 is empty & proj1 .: C2 is bounded_below holds W-bound S = min ((W-bound C1),(W-bound C2)) proofend; Lm7: for p being Point of (TOP-REAL 2) for X being Subset of (TOP-REAL 2) st p in X & X is bounded holds ( lower_bound (proj1 | X) <= p `1 & p `1 <= upper_bound (proj1 | X) ) proofend; Lm8: for p being Point of (TOP-REAL 2) for X being Subset of (TOP-REAL 2) st p in X & X is bounded holds ( lower_bound (proj2 | X) <= p `2 & p `2 <= upper_bound (proj2 | X) ) proofend; theorem Th5: :: JORDAN1C:5 for p being Point of (TOP-REAL 2) for X being Subset of (TOP-REAL 2) st p in X & X is bounded holds ( W-bound X <= p `1 & p `1 <= E-bound X & S-bound X <= p `2 & p `2 <= N-bound X ) proofend; Lm9: for C being Subset of (TOP-REAL 2) st C is bounded holds for h being real number st BDD C <> {} & h > W-bound (BDD C) holds ex p being Point of (TOP-REAL 2) st ( p in BDD C & not p `1 >= h ) proofend; Lm10: for C being Subset of (TOP-REAL 2) st C is bounded holds for h being real number st BDD C <> {} & h < E-bound (BDD C) holds ex p being Point of (TOP-REAL 2) st ( p in BDD C & not p `1 <= h ) proofend; Lm11: for C being Subset of (TOP-REAL 2) st C is bounded holds for h being real number st BDD C <> {} & h < N-bound (BDD C) holds ex p being Point of (TOP-REAL 2) st ( p in BDD C & not p `2 <= h ) proofend; Lm12: for C being Subset of (TOP-REAL 2) st C is bounded holds for h being real number st BDD C <> {} & h > S-bound (BDD C) holds ex p being Point of (TOP-REAL 2) st ( p in BDD C & not p `2 >= h ) proofend; Lm13: now__::_thesis:_for_C_being_Subset_of_(TOP-REAL_2)_st_C_is_bounded_holds_ not_UBD_C_is_empty let C be Subset of (TOP-REAL 2); ::_thesis: ( C is bounded implies not UBD C is empty ) assume C is bounded ; ::_thesis: not UBD C is empty then UBD C is_outside_component_of C by JORDAN2C:68; hence not UBD C is empty by JORDAN2C:def_3; ::_thesis: verum end; theorem Th6: :: JORDAN1C:6 for C being compact Subset of (TOP-REAL 2) st BDD C <> {} holds W-bound C <= W-bound (BDD C) proofend; theorem Th7: :: JORDAN1C:7 for C being compact Subset of (TOP-REAL 2) st BDD C <> {} holds E-bound C >= E-bound (BDD C) proofend; theorem Th8: :: JORDAN1C:8 for C being compact Subset of (TOP-REAL 2) st BDD C <> {} holds S-bound C <= S-bound (BDD C) proofend; theorem Th9: :: JORDAN1C:9 for C being compact Subset of (TOP-REAL 2) st BDD C <> {} holds N-bound C >= N-bound (BDD C) proofend; theorem Th10: :: JORDAN1C:10 for n being Element of NAT for p being Point of (TOP-REAL 2) for C being compact non vertical Subset of (TOP-REAL 2) for I being Integer st p in BDD C & I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds 1 < I proofend; theorem Th11: :: JORDAN1C:11 for n being Element of NAT for p being Point of (TOP-REAL 2) for C being compact non vertical Subset of (TOP-REAL 2) for I being Integer st p in BDD C & I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds I + 1 <= len (Gauge (C,n)) proofend; theorem Th12: :: JORDAN1C:12 for n being Element of NAT for p being Point of (TOP-REAL 2) for C being compact non horizontal Subset of (TOP-REAL 2) for J being Integer st p in BDD C & J = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] holds ( 1 < J & J + 1 <= width (Gauge (C,n)) ) proofend; theorem Th13: :: JORDAN1C:13 for C being Simple_closed_curve for n being Element of NAT for p being Point of (TOP-REAL 2) for I being Integer st I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2)) <= p `1 proofend; theorem Th14: :: JORDAN1C:14 for C being Simple_closed_curve for n being Element of NAT for p being Point of (TOP-REAL 2) for I being Integer st I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds p `1 < (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 1)) proofend; theorem Th15: :: JORDAN1C:15 for C being Simple_closed_curve for n being Element of NAT for p being Point of (TOP-REAL 2) for J being Integer st J = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] holds (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 2)) <= p `2 proofend; theorem Th16: :: JORDAN1C:16 for C being Simple_closed_curve for n being Element of NAT for p being Point of (TOP-REAL 2) for J being Integer st J = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] holds p `2 < (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 1)) proofend; theorem Th17: :: JORDAN1C:17 for C being closed Subset of (TOP-REAL 2) for p being Point of (Euclid 2) st p in BDD C holds ex r being Real st ( r > 0 & Ball (p,r) c= BDD C ) proofend; theorem :: JORDAN1C:18 for C being Simple_closed_curve for n, i, j being Element of NAT for p, q being Point of (TOP-REAL 2) for r being real number st dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < r & p in cell ((Gauge (C,n)),i,j) & q in cell ((Gauge (C,n)),i,j) & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) holds dist (p,q) < 2 * r proofend; theorem :: JORDAN1C:19 for p being Point of (TOP-REAL 2) for C being compact Subset of (TOP-REAL 2) st p in BDD C holds p `2 <> N-bound (BDD C) proofend; theorem :: JORDAN1C:20 for p being Point of (TOP-REAL 2) for C being compact Subset of (TOP-REAL 2) st p in BDD C holds p `1 <> E-bound (BDD C) proofend; theorem :: JORDAN1C:21 for p being Point of (TOP-REAL 2) for C being compact Subset of (TOP-REAL 2) st p in BDD C holds p `2 <> S-bound (BDD C) proofend; theorem Th22: :: JORDAN1C:22 for p being Point of (TOP-REAL 2) for C being compact Subset of (TOP-REAL 2) st p in BDD C holds p `1 <> W-bound (BDD C) proofend; theorem :: JORDAN1C:23 for C being Simple_closed_curve for p being Point of (TOP-REAL 2) st p in BDD C holds ex n, i, j being Element of NAT st ( 1 < i & i < len (Gauge (C,n)) & 1 < j & j < width (Gauge (C,n)) & p `1 <> ((Gauge (C,n)) * (i,j)) `1 & p in cell ((Gauge (C,n)),i,j) & cell ((Gauge (C,n)),i,j) c= BDD C ) proofend; theorem :: JORDAN1C:24 for C being Subset of (TOP-REAL 2) st C is bounded holds not UBD C is empty by Lm13;