:: Some Properties of Cells and Gauges
:: by Adam Grabowski , Artur Korni{\l}owicz and Andrzej Trybulec
::
:: Received October 13, 2000
:: Copyright (c) 2000 Association of Mizar Users
Lm2:
for a, b, c being real number st a <> 0 & b <> 0 holds
(a / b) * ((c / a) * b) = c
Lm3:
for p being Point of (TOP-REAL 2) holds p is Point of (Euclid 2)
Lm4:
for r being real number st r > 0 holds
2 * (r / 4) < r
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 )
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 )
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 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 & (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
theorem Th4: :: JORDAN1C:4
theorem :: JORDAN1C:5
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) )
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) )
theorem Th6: :: JORDAN1C:6
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 )
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 )
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 )
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 )
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
theorem Th19: :: JORDAN1C:19
theorem Th20: :: JORDAN1C:20
theorem Th21: :: JORDAN1C:21
theorem Th22: :: JORDAN1C:22
theorem Th23: :: JORDAN1C:23
theorem Th24: :: JORDAN1C:24
theorem Th25: :: JORDAN1C:25
theorem Th26: :: JORDAN1C:26
theorem Th27: :: JORDAN1C:27
theorem Th28: :: JORDAN1C:28
theorem Th29: :: JORDAN1C:29
theorem Th30: :: 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
theorem :: JORDAN1C:31
theorem :: JORDAN1C:32
theorem :: JORDAN1C:33
theorem Th34: :: JORDAN1C:34
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 )
theorem :: JORDAN1C:36