begin
theorem Th4:
for
n being
Element of
NAT for
r being
real number for
y,
z being
Point of
(TOP-REAL n) for
x being
set st
x = ((1 - r) * y) + (r * z) holds
( ( not
x = y or
r = 0 or
y = z ) & ( (
r = 0 or
y = z ) implies
x = y ) & ( not
x = z or
r = 1 or
y = z ) & ( (
r = 1 or
y = z ) implies
x = z ) )
begin
Lm1:
for n being Element of NAT
for a being real number
for P being Subset of (TOP-REAL n)
for Q being Point of (TOP-REAL n) st P = { q where q is Point of (TOP-REAL n) : |.(q - Q).| <= a } holds
P is convex
Lm2:
for n being Element of NAT
for a being real number
for P being Subset of (TOP-REAL n)
for Q being Point of (TOP-REAL n) st P = { q where q is Point of (TOP-REAL n) : |.(q - Q).| < a } holds
P is convex
theorem Th37:
for
n being
Element of
NAT for
r,
a being
real number for
y,
z,
x being
Point of
(TOP-REAL n) for
S,
T,
X being
Element of
REAL n st
S = y &
T = z &
X = x &
y <> z &
y in Ball (
x,
r) &
a = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) holds
ex
e being
Point of
(TOP-REAL n) st
(
{e} = (halfline (y,z)) /\ (Sphere (x,r)) &
e = ((1 - a) * y) + (a * z) )
theorem Th38:
for
n being
Element of
NAT for
r,
a being
real number for
y,
z,
x being
Point of
(TOP-REAL n) for
S,
T,
Y being
Element of
REAL n st
S = ((1 / 2) * y) + ((1 / 2) * z) &
T = z &
Y = x &
y <> z &
y in Sphere (
x,
r) &
z in cl_Ball (
x,
r) holds
ex
e being
Point of
(TOP-REAL n) st
(
e <> y &
{y,e} = (halfline (y,z)) /\ (Sphere (x,r)) & (
z in Sphere (
x,
r) implies
e = z ) & ( not
z in Sphere (
x,
r) &
a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies
e = ((1 - a) * (((1 / 2) * y) + ((1 / 2) * z))) + (a * z) ) )
begin
theorem
for
a,
b,
w,
r being
real number for
s,
t being
Point of
(TOP-REAL 2) for
S,
T,
X being
Element of
REAL 2 st
S = s &
T = t &
X = |[a,b]| &
w = ((- (2 * |((t - s),(s - |[a,b]|))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - |[a,b]|))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) &
s <> t &
s in inside_of_circle (
a,
b,
r) holds
ex
e being
Point of
(TOP-REAL 2) st
(
{e} = (halfline (s,t)) /\ (circle (a,b,r)) &
e = ((1 - w) * s) + (w * t) )
theorem
for
a,
b,
r being
real number for
s,
t being
Point of
(TOP-REAL 2) st
s in circle (
a,
b,
r) &
t in inside_of_circle (
a,
b,
r) holds
(LSeg (s,t)) /\ (circle (a,b,r)) = {s}
theorem
for
a,
b,
r being
real number for
s,
t being
Point of
(TOP-REAL 2) st
s in circle (
a,
b,
r) &
t in circle (
a,
b,
r) holds
(LSeg (s,t)) \ {s,t} c= inside_of_circle (
a,
b,
r)
theorem
for
a,
b,
r being
real number for
s,
t being
Point of
(TOP-REAL 2) st
s in circle (
a,
b,
r) &
t in circle (
a,
b,
r) holds
(LSeg (s,t)) /\ (circle (a,b,r)) = {s,t}
theorem
for
a,
b,
r being
real number for
s,
t being
Point of
(TOP-REAL 2) st
s in circle (
a,
b,
r) &
t in circle (
a,
b,
r) holds
(halfline (s,t)) /\ (circle (a,b,r)) = {s,t}
theorem
for
a,
b,
r,
w being
real number for
s,
t being
Point of
(TOP-REAL 2) for
S,
T,
Y being
Element of
REAL 2 st
S = ((1 / 2) * s) + ((1 / 2) * t) &
T = t &
Y = |[a,b]| &
s <> t &
s in circle (
a,
b,
r) &
t in closed_inside_of_circle (
a,
b,
r) holds
ex
e being
Point of
(TOP-REAL 2) st
(
e <> s &
{s,e} = (halfline (s,t)) /\ (circle (a,b,r)) & (
t in Sphere (
|[a,b]|,
r) implies
e = t ) & ( not
t in Sphere (
|[a,b]|,
r) &
w = ((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies
e = ((1 - w) * (((1 / 2) * s) + ((1 / 2) * t))) + (w * t) ) )