:: JORDAN1C semantic presentation

Lm1: now

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

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 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 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) = TOP-REAL 2
by EUCLID:def 8;

then Lm5: 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 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 & (Gauge C,n) * i,j in Ball q,r & (Gauge C,n) * (i + 1),j in Ball q,r & (Gauge C,n) * i,(j + 1) in Ball q,r & (Gauge C,n) * (i + 1),(j + 1) in Ball q,r 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
( inf (proj1 || X) <= p `1 & p `1 <= sup (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
( inf (proj2 || X) <= p `2 & p `2 <= sup (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;

theorem :: JORDAN1C:7

for p being Point of (TOP-REAL 2) holds
( p in west_halfline p & p in east_halfline p & p in north_halfline p & p in south_halfline p )

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;

theorem Th8: :: JORDAN1C:8

for p being Point of (TOP-REAL 2) holds not west_halfline p is Bounded

proof end;

theorem Th9: :: JORDAN1C:9

for p being Point of (TOP-REAL 2) holds not east_halfline p is Bounded

proof end;

theorem Th10: :: JORDAN1C:10

for p being Point of (TOP-REAL 2) holds not north_halfline p is Bounded

proof end;

theorem Th11: :: JORDAN1C:11

for p being Point of (TOP-REAL 2) holds not south_halfline p is Bounded

proof end;

Lm13: now

let C be Subset of (TOP-REAL 2); :: thesis:
assume A1: C is Bounded ; :: thesis:
then consider B being Subset of (TOP-REAL 2) such that
A2: B is_outside_component_of C and
A3: B = UBD C by JORDAN2C:76;
A4: UBD C is_a_component_of C ` by A2, A3, JORDAN2C:def 4;
C ` <> {} by A1, JORDAN2C:74;
hence not UBD C is empty by A4, SPRECT_1:6; :: thesis:

end;

registration

let C be compact Subset of (TOP-REAL 2);
cluster UBD C -> non empty ;
coherence

proof end;

end;

theorem Th12: :: JORDAN1C:12

for C being compact Subset of (TOP-REAL 2) holds UBD C is_a_component_of C `

proof end;

theorem Th13: :: JORDAN1C:13

for C being compact Subset of (TOP-REAL 2)
for WH being connected Subset of (TOP-REAL 2) st not WH is Bounded & WH misses C holds
WH c= UBD C

proof end;

theorem Th14: :: JORDAN1C:14

for C being compact Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st west_halfline p misses C holds
west_halfline p c= UBD C

proof end;

theorem Th15: :: JORDAN1C:15

for C being compact Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st east_halfline p misses C holds
east_halfline p c= UBD C

proof end;

theorem Th16: :: JORDAN1C:16

for C being compact Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st south_halfline p misses C holds
south_halfline p c= UBD C

proof end;

theorem Th17: :: JORDAN1C:17

for C being compact Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st north_halfline p misses C holds
north_halfline p c= UBD C

proof end;

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

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