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

Lm1: now :: thesis: for r being Real
for j being Nat holds [\(r + j)/] - j = [\r/]
let r be Real; :: thesis: for j being Nat holds [\(r + j)/] - j = [\r/]
let j be 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 st a <> 0 & b <> 0 holds
(a / b) * ((c / a) * b) = c

proof end;

Lm3: for p being Point of () holds p is Point of ()
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 () = TopStruct(# the carrier of (), the topology of () #)
by EUCLID:def 8;

then Lm5: TopStruct(# the carrier of (), the topology of () #) = TopStruct(# the carrier of (),() #)
by PCOMPS_1:def 5;

Lm6: for C being Simple_closed_curve
for i, j, n being Nat
for p being Point of ()
for r being Real
for q being Point of () 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 () st S is bounded holds
proj1 .: S is real-bounded
proof end;

theorem :: JORDAN1C:4
for C1 being non empty compact Subset of ()
for C2, S being non empty Subset of () 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 ()
for X being Subset of () st p in X & X is bounded holds
( lower_bound () <= p 1 & p 1 <= upper_bound () )

proof end;

Lm8: for p being Point of ()
for X being Subset of () st p in X & X is bounded holds
( lower_bound () <= p 2 & p 2 <= upper_bound () )

proof end;

theorem Th5: :: JORDAN1C:5
for p being Point of ()
for X being Subset of () 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 () st C is bounded holds
for h being Real st BDD C <> {} & h > W-bound (BDD C) holds
ex p being Point of () st
( p in BDD C & not p 1 >= h )

proof end;

Lm10: for C being Subset of () st C is bounded holds
for h being Real st BDD C <> {} & h < E-bound (BDD C) holds
ex p being Point of () st
( p in BDD C & not p 1 <= h )

proof end;

Lm11: for C being Subset of () st C is bounded holds
for h being Real st BDD C <> {} & h < N-bound (BDD C) holds
ex p being Point of () st
( p in BDD C & not p 2 <= h )

proof end;

Lm12: for C being Subset of () st C is bounded holds
for h being Real st BDD C <> {} & h > S-bound (BDD C) holds
ex p being Point of () st
( p in BDD C & not p 2 >= h )

proof end;

Lm13: now :: thesis: for C being Subset of () st C is bounded holds
not UBD C is empty
let C be Subset of (); :: 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 () st BDD C <> {} holds
W-bound C <= W-bound (BDD C)
proof end;

theorem Th7: :: JORDAN1C:7
for C being compact Subset of () st BDD C <> {} holds
E-bound C >= E-bound (BDD C)
proof end;

theorem Th8: :: JORDAN1C:8
for C being compact Subset of () st BDD C <> {} holds
S-bound C <= S-bound (BDD C)
proof end;

theorem Th9: :: JORDAN1C:9
for C being compact Subset of () 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 ()
for C being compact non vertical Subset of ()
for I being Integer st p in BDD C & I = [\(((((p 1) - ()) / (() - ())) * (2 |^ n)) + 2)/] holds
1 < I
proof end;

theorem Th11: :: JORDAN1C:11
for n being Nat
for p being Point of ()
for C being compact non vertical Subset of ()
for I being Integer st p in BDD C & I = [\(((((p 1) - ()) / (() - ())) * (2 |^ n)) + 2)/] holds
I + 1 <= len (Gauge (C,n))
proof end;

theorem Th12: :: JORDAN1C:12
for n being Nat
for p being Point of ()
for C being compact non horizontal Subset of ()
for J being Integer st p in BDD C & J = [\(((((p 2) - ()) / (() - ())) * (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 ()
for I being Integer st I = [\(((((p 1) - ()) / (() - ())) * (2 |^ n)) + 2)/] holds
() + (((() - ()) / (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 ()
for I being Integer st I = [\(((((p 1) - ()) / (() - ())) * (2 |^ n)) + 2)/] holds
p 1 < () + (((() - ()) / (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 ()
for J being Integer st J = [\(((((p 2) - ()) / (() - ())) * (2 |^ n)) + 2)/] holds
() + (((() - ()) / (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 ()
for J being Integer st J = [\(((((p 2) - ()) / (() - ())) * (2 |^ n)) + 2)/] holds
p 2 < () + (((() - ()) / (2 |^ n)) * (J - 1))
proof end;

theorem Th17: :: JORDAN1C:17
for C being closed Subset of ()
for p being Point of () 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 ()
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 ()
for C being compact Subset of () st p in BDD C holds
p 2 <> N-bound (BDD C)
proof end;

theorem :: JORDAN1C:20
for p being Point of ()
for C being compact Subset of () st p in BDD C holds
p 1 <> E-bound (BDD C)
proof end;

theorem :: JORDAN1C:21
for p being Point of ()
for C being compact Subset of () st p in BDD C holds
p 2 <> S-bound (BDD C)
proof end;

theorem Th22: :: JORDAN1C:22
for p being Point of ()
for C being compact Subset of () 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 () 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 () st C is bounded holds
not UBD C is empty by Lm13;