begin
theorem
theorem Th2:
theorem Th3:
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 ) )
theorem Th5:
theorem Th6:
begin
:: deftheorem defines Ball TOPREAL9:def 1 :
for n being Nat
for x being Point of (TOP-REAL n)
for r being real number holds Ball x,r = { p where p is Point of (TOP-REAL n) : |.(p - x).| < r } ;
:: deftheorem defines cl_Ball TOPREAL9:def 2 :
for n being Nat
for x being Point of (TOP-REAL n)
for r being real number holds cl_Ball x,r = { p where p is Point of (TOP-REAL n) : |.(p - x).| <= r } ;
:: deftheorem defines Sphere TOPREAL9:def 3 :
for n being Nat
for x being Point of (TOP-REAL n)
for r being real number holds Sphere x,r = { p where p is Point of (TOP-REAL n) : |.(p - x).| = r } ;
theorem Th7:
theorem Th8:
theorem Th9:
theorem
theorem
theorem
theorem Th13:
theorem Th14:
theorem Th15:
theorem
theorem Th17:
theorem Th18:
theorem Th19:
theorem
theorem
theorem
theorem
theorem Th24:
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
:: deftheorem Def4 defines homogeneous TOPREAL9:def 4 :
for n being Nat
for f being Function of (TOP-REAL n),(TOP-REAL n) holds
( f is homogeneous iff for r being real number
for x being Point of (TOP-REAL n) holds f . (r * x) = r * (f . x) );
:: deftheorem TOPREAL9:def 5 :
canceled;
registration
let a,
c be
real number ;
cluster AffineMap a,
0 ,
c,
0 -> additive homogeneous ;
coherence
( AffineMap a,0 ,c,0 is homogeneous & AffineMap a,0 ,c,0 is additive )
end;
theorem
:: deftheorem defines halfline TOPREAL9:def 6 :
for n being Nat
for p, q being Point of (TOP-REAL n) holds halfline p,q = { (((1 - l) * p) + (l * q)) where l is Real : 0 <= l } ;
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem
theorem
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
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) ) )
theorem
theorem
begin
theorem
theorem
theorem Th43:
theorem Th44:
theorem Th45:
theorem
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem
theorem Th52:
theorem
theorem
theorem
theorem
theorem
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) ) )
registration
let a,
b,
r be
real number ;
cluster inside_of_circle a,
b,
r -> convex ;
coherence
inside_of_circle a,b,r is convex
cluster closed_inside_of_circle a,
b,
r -> convex ;
coherence
closed_inside_of_circle a,b,r is convex
end;