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

begin

Lm1: now

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:51
.= [\r/] ; :: thesis: verum

end;

Lm2: for a, b, c being real number 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 number st r > 0 holds
2 * (r / 4) < r

proof end;

theorem :: JORDAN1C:1

canceled;

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 + 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 Th3: :: JORDAN1C:3

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)

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 6;

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)

proof end;

theorem Th4: :: JORDAN1C:4

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

proof end;

theorem :: JORDAN1C:5

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 Th6: :: JORDAN1C:6

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

proof end;

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 )

proof end;

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 )

proof end;

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 )

proof end;

Lm13: now

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:76;
hence not UBD C is empty by JORDAN2C:def 4; :: thesis: verum

end;

theorem :: JORDAN1C:7

canceled;

theorem :: JORDAN1C:8

canceled;

theorem :: JORDAN1C:9

canceled;

theorem :: JORDAN1C:10

canceled;

theorem :: JORDAN1C:11

canceled;

theorem :: JORDAN1C:12

canceled;

theorem :: JORDAN1C:13

canceled;

theorem :: JORDAN1C:14

canceled;

theorem :: JORDAN1C:15

canceled;

theorem :: JORDAN1C:16

canceled;

theorem :: JORDAN1C:17

canceled;

theorem Th18: :: JORDAN1C:18

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

proof end;

theorem Th19: :: JORDAN1C:19

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

proof end;

theorem Th20: :: JORDAN1C:20

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

proof end;

theorem Th21: :: JORDAN1C:21

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

proof end;

theorem Th22: :: JORDAN1C:22

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

proof end;

theorem Th23: :: JORDAN1C:23

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

proof end;

theorem Th24: :: JORDAN1C:24

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

proof end;

theorem Th25: :: JORDAN1C:25

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

proof end;

theorem Th26: :: JORDAN1C:26

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

proof end;

theorem Th27: :: JORDAN1C:27

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

proof end;

theorem Th28: :: JORDAN1C:28

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

proof end;

theorem Th29: :: JORDAN1C:29

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:30

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

proof end;

theorem :: JORDAN1C:31

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:32

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:33

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 Th34: :: JORDAN1C:34

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:35

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 )

proof end;

theorem :: JORDAN1C:36

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