:: by Adam Grabowski , Artur Korni{\l}owicz and Andrzej Trybulec

::

:: Received October 13, 2000

:: Copyright (c) 2000-2017 Association of Mizar Users

Lm1: now :: thesis: for r being Real

for j being Nat holds [\(r + j)/] - j = [\r/]

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;
let j be Nat; :: thesis: [\(r + j)/] - j = [\r/]

thus [\(r + j)/] - j = ([\r/] + j) - j by INT_1:28

.= [\r/] ; :: thesis: verum

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)

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)

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

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 )

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

not UBD C is empty

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

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

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

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

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

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

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

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

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

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 )

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

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)

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)

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)

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)

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 )

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