begin
Lm1:
for r being real number
for X being Subset of (TOP-REAL 2) st r in proj2 .: X holds
ex x being Point of (TOP-REAL 2) st
( x in X & proj2 . x = r )
theorem Th1:
theorem Th2:
theorem
theorem
Lm2:
dom proj2 = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
Lm3:
for R being non empty Subset of (TOP-REAL 2)
for n being Element of NAT holds 1 <= len (Gauge R,n)
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
for
i,
m,
k,
j being
Element of
NAT for
C being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st
m > k &
[i,j] in Indices (Gauge C,k) &
[i,(j + 1)] in Indices (Gauge C,k) holds
dist ((Gauge C,m) * i,j),
((Gauge C,m) * i,(j + 1)) < dist ((Gauge C,k) * i,j),
((Gauge C,k) * i,(j + 1))
theorem Th9:
for
m,
k being
Element of
NAT for
C being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st
m > k holds
dist ((Gauge C,m) * 1,1),
((Gauge C,m) * 1,2) < dist ((Gauge C,k) * 1,1),
((Gauge C,k) * 1,2)
theorem Th10:
for
i,
m,
k,
j being
Element of
NAT for
C being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st
m > k &
[i,j] in Indices (Gauge C,k) &
[(i + 1),j] in Indices (Gauge C,k) holds
dist ((Gauge C,m) * i,j),
((Gauge C,m) * (i + 1),j) < dist ((Gauge C,k) * i,j),
((Gauge C,k) * (i + 1),j)
theorem Th11:
for
m,
k being
Element of
NAT for
C being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st
m > k holds
dist ((Gauge C,m) * 1,1),
((Gauge C,m) * 2,1) < dist ((Gauge C,k) * 1,1),
((Gauge C,k) * 2,1)
theorem
for
C being
Simple_closed_curve for
i being
Element of
NAT for
r,
t being
real number st
r > 0 &
t > 0 holds
ex
n being
Element of
NAT st
(
i < n &
dist ((Gauge C,n) * 1,1),
((Gauge C,n) * 1,2) < r &
dist ((Gauge C,n) * 1,1),
((Gauge C,n) * 2,1) < t )
theorem Th13:
for
C being
Simple_closed_curve for
n being
Element of
NAT st
0 < n holds
sup (proj2 .: ((L~ (Cage C,n)) /\ (LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n)))))) = sup (proj2 .: ((L~ (Cage C,n)) /\ (Vertical_Line (((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2))))
theorem Th14:
for
C being
Simple_closed_curve for
n being
Element of
NAT st
0 < n holds
inf (proj2 .: ((L~ (Cage C,n)) /\ (LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n)))))) = inf (proj2 .: ((L~ (Cage C,n)) /\ (Vertical_Line (((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2))))
theorem
for
C being
Simple_closed_curve for
n being
Element of
NAT st
0 < n holds
UMP (L~ (Cage C,n)) = |[(((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2),(sup (proj2 .: ((L~ (Cage C,n)) /\ (LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n)))))))]| by Th13;
theorem
for
C being
Simple_closed_curve for
n being
Element of
NAT st
0 < n holds
LMP (L~ (Cage C,n)) = |[(((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2),(inf (proj2 .: ((L~ (Cage C,n)) /\ (LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n)))))))]| by Th14;
theorem Th17:
theorem Th18:
theorem
canceled;
theorem
canceled;
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
begin
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
Lm4:
TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2)
by EUCLID:def 8;
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem
theorem
theorem
theorem
theorem