begin
begin
Lm1:
for n being Nat
for r being Real st r > 0 holds
for x, y, z being Element of (Euclid n) st x = 0* n holds
for p being Element of (TOP-REAL n) st p = y & r * p = z holds
r * (dist (x,y)) = dist (x,z)
Lm2:
for n being Nat
for r, s being Real st r > 0 holds
for x being Element of (Euclid n) st x = 0* n holds
for A being Subset of (TOP-REAL n) st A = Ball (x,s) holds
r * A = Ball (x,(r * s))
Lm3:
for n being Nat
for r, s, t being Real st 0 < s & s <= t holds
for x being Element of (Euclid n) st x = 0* n holds
for BA being Subset of (TOP-REAL n) st BA = Ball (x,r) holds
s * BA c= t * BA
theorem Th40:
for
n being
Element of
NAT for
P being
Subset of
(TOP-REAL n) for
w1,
w2,
w3,
w4,
w5,
w6,
w7 being
Point of
(TOP-REAL n) st
w1 in P &
w2 in P &
w3 in P &
w4 in P &
w5 in P &
w6 in P &
w7 in P &
LSeg (
w1,
w2)
c= P &
LSeg (
w2,
w3)
c= P &
LSeg (
w3,
w4)
c= P &
LSeg (
w4,
w5)
c= P &
LSeg (
w5,
w6)
c= P &
LSeg (
w6,
w7)
c= P holds
ex
h being
Function of
I[01],
((TOP-REAL n) | P) st
(
h is
continuous &
w1 = h . 0 &
w7 = h . 1 )
theorem Th48:
for
n being
Element of
NAT for
a being
Real for
Q being
Subset of
(TOP-REAL n) for
w1,
w7 being
Point of
(TOP-REAL n) st
n >= 2 &
Q = { q where q is Point of (TOP-REAL n) : |.q.| > a } &
w1 in Q &
w7 in Q & ex
r being
Real st
(
w1 = r * w7 or
w7 = r * w1 ) holds
ex
w2,
w3,
w4,
w5,
w6 being
Point of
(TOP-REAL n) st
(
w2 in Q &
w3 in Q &
w4 in Q &
w5 in Q &
w6 in Q &
LSeg (
w1,
w2)
c= Q &
LSeg (
w2,
w3)
c= Q &
LSeg (
w3,
w4)
c= Q &
LSeg (
w4,
w5)
c= Q &
LSeg (
w5,
w6)
c= Q &
LSeg (
w6,
w7)
c= Q )
theorem Th49:
for
n being
Element of
NAT for
a being
Real for
Q being
Subset of
(TOP-REAL n) for
w1,
w7 being
Point of
(TOP-REAL n) st
n >= 2 &
Q = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } &
w1 in Q &
w7 in Q & ex
r being
Real st
(
w1 = r * w7 or
w7 = r * w1 ) holds
ex
w2,
w3,
w4,
w5,
w6 being
Point of
(TOP-REAL n) st
(
w2 in Q &
w3 in Q &
w4 in Q &
w5 in Q &
w6 in Q &
LSeg (
w1,
w2)
c= Q &
LSeg (
w2,
w3)
c= Q &
LSeg (
w3,
w4)
c= Q &
LSeg (
w4,
w5)
c= Q &
LSeg (
w5,
w6)
c= Q &
LSeg (
w6,
w7)
c= Q )
begin
begin
begin