JORDAN1C: Some Properties of Cells and Gauges

:: Some Properties of Cells and Gauges
:: by Adam Grabowski , Artur Korni{\l}owicz and Andrzej Trybulec
::
:: Received October 13, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users

Lm1: now :: thesis:

let r be Real; :: thesis:
let j be Nat; :: thesis:
thus [\(r + j)/] - j = ([\r/] + j) - j by INT_1:28
.= [\r/] ; :: thesis:

end;

Lm2: for a, b, c being Real st a <> 0 & b <> 0 holds
(a / b) * ((c / a) * b) = c

proof end;

Lm3: for p being Point of (TOP-REAL 2) holds p is Point of (Euclid 2)

proof end;

Lm4: for r being Real st r > 0 holds
2 * (r / 4) < r

proof end;

theorem Th1: :: JORDAN1C:1

for C being Simple_closed_curve
for i, j, n being 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)

proof end;

theorem Th2: :: JORDAN1C:2

for C being Simple_closed_curve
for i, j, n being 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)

proof end;

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, j, n being Nat
for p being Point of (TOP-REAL 2)
for r being Real
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)

proof end;

theorem Th3: :: JORDAN1C:3

for S being Subset of (TOP-REAL 2) st S is bounded holds
proj1 .: S is real-bounded

proof end;

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))

proof end;

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) )

proof end;

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) )

proof end;

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 )

proof end;

Lm9: for C being Subset of (TOP-REAL 2) st C is bounded holds
for h being Real 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 )

proof end;

Lm10: for C being Subset of (TOP-REAL 2) st C is bounded holds
for h being Real 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 )

proof end;

Lm11: for C being Subset of (TOP-REAL 2) st C is bounded holds
for h being Real 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 )

proof end;

Lm12: for C being Subset of (TOP-REAL 2) st C is bounded holds
for h being Real 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 )

proof end;

Lm13: now :: thesis:

let C be Subset of (TOP-REAL 2); :: thesis:
assume C is bounded ; :: thesis:
then UBD C is_outside_component_of C by JORDAN2C:68;
hence not UBD C is empty by JORDAN2C:def 3; :: thesis:

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)

proof end;

theorem Th7: :: JORDAN1C:7

for C being compact Subset of (TOP-REAL 2) st BDD C <> {} holds
E-bound C >= E-bound (BDD C)

proof end;

theorem Th8: :: JORDAN1C:8

for C being compact Subset of (TOP-REAL 2) st BDD C <> {} holds
S-bound C <= S-bound (BDD C)

proof end;

theorem Th9: :: JORDAN1C:9

for C being compact Subset of (TOP-REAL 2) st BDD C <> {} holds
N-bound C >= N-bound (BDD C)

proof end;

theorem Th10: :: JORDAN1C:10

for n being 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

proof end;

theorem Th11: :: JORDAN1C:11

proof end;

theorem Th12: :: JORDAN1C:12

for n being 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)) )

proof end;

theorem Th13: :: JORDAN1C:13

for C being Simple_closed_curve
for n being 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

proof end;

theorem Th14: :: JORDAN1C:14

for C being Simple_closed_curve
for n being 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))

proof end;

theorem Th15: :: JORDAN1C:15

for C being Simple_closed_curve
for n being 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

proof end;

theorem Th16: :: JORDAN1C:16

for C being Simple_closed_curve
for n being 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))

proof end;

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 )

proof end;

theorem :: JORDAN1C:18

for C being Simple_closed_curve
for i, j, n being Nat
for p, q being Point of (TOP-REAL 2)
for r being Real 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

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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 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 )

proof end;

theorem :: JORDAN1C:24

for C being Subset of (TOP-REAL 2) st C is bounded holds
not UBD C is empty by Lm13;