:: by Artur Korni{\l}owicz and Yasunari Shidama

::

:: Received May 10, 2004

:: Copyright (c) 2004-2018 Association of Mizar Users

::$CT 2

theorem Th2: :: TOPREAL9:4

for r being Real

for V being RealLinearSpace

for y, z being Point of V

for x being object 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 ) )

for V being RealLinearSpace

for y, z being Point of V

for x being object 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 ) )

proof end;

theorem Th4: :: TOPREAL9:6

for r being Real

for M being non empty MetrSpace

for z1, z2, z3 being Point of M st z1 <> z2 & z1 in cl_Ball (z3,r) & z2 in cl_Ball (z3,r) holds

r > 0

for M being non empty MetrSpace

for z1, z2, z3 being Point of M st z1 <> z2 & z1 in cl_Ball (z3,r) & z2 in cl_Ball (z3,r) holds

r > 0

proof end;

definition

let n be Nat;

let x be Point of (TOP-REAL n);

let r be Real;

{ p where p is Point of (TOP-REAL n) : |.(p - x).| < r } is Subset of (TOP-REAL n)

{ p where p is Point of (TOP-REAL n) : |.(p - x).| <= r } is Subset of (TOP-REAL n)

{ p where p is Point of (TOP-REAL n) : |.(p - x).| = r } is Subset of (TOP-REAL n)

end;
let x be Point of (TOP-REAL n);

let r be Real;

func Ball (x,r) -> Subset of (TOP-REAL n) equals :: TOPREAL9:def 1

{ p where p is Point of (TOP-REAL n) : |.(p - x).| < r } ;

coherence { p where p is Point of (TOP-REAL n) : |.(p - x).| < r } ;

{ p where p is Point of (TOP-REAL n) : |.(p - x).| < r } is Subset of (TOP-REAL n)

proof end;

func cl_Ball (x,r) -> Subset of (TOP-REAL n) equals :: TOPREAL9:def 2

{ p where p is Point of (TOP-REAL n) : |.(p - x).| <= r } ;

coherence { p where p is Point of (TOP-REAL n) : |.(p - x).| <= r } ;

{ p where p is Point of (TOP-REAL n) : |.(p - x).| <= r } is Subset of (TOP-REAL n)

proof end;

func Sphere (x,r) -> Subset of (TOP-REAL n) equals :: TOPREAL9:def 3

{ p where p is Point of (TOP-REAL n) : |.(p - x).| = r } ;

coherence { p where p is Point of (TOP-REAL n) : |.(p - x).| = r } ;

{ p where p is Point of (TOP-REAL n) : |.(p - x).| = r } is Subset of (TOP-REAL n)

proof end;

:: deftheorem defines Ball TOPREAL9:def 1 :

for n being Nat

for x being Point of (TOP-REAL n)

for r being Real holds Ball (x,r) = { p where p is Point of (TOP-REAL n) : |.(p - x).| < r } ;

for n being Nat

for x being Point of (TOP-REAL n)

for r being Real 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 holds cl_Ball (x,r) = { p where p is Point of (TOP-REAL n) : |.(p - x).| <= r } ;

for n being Nat

for x being Point of (TOP-REAL n)

for r being Real 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 holds Sphere (x,r) = { p where p is Point of (TOP-REAL n) : |.(p - x).| = r } ;

for n being Nat

for x being Point of (TOP-REAL n)

for r being Real holds Sphere (x,r) = { p where p is Point of (TOP-REAL n) : |.(p - x).| = r } ;

theorem Th5: :: TOPREAL9:7

for n being Nat

for r being Real

for x, y being Point of (TOP-REAL n) holds

( y in Ball (x,r) iff |.(y - x).| < r )

for r being Real

for x, y being Point of (TOP-REAL n) holds

( y in Ball (x,r) iff |.(y - x).| < r )

proof end;

theorem Th6: :: TOPREAL9:8

for n being Nat

for r being Real

for x, y being Point of (TOP-REAL n) holds

( y in cl_Ball (x,r) iff |.(y - x).| <= r )

for r being Real

for x, y being Point of (TOP-REAL n) holds

( y in cl_Ball (x,r) iff |.(y - x).| <= r )

proof end;

theorem Th7: :: TOPREAL9:9

for n being Nat

for r being Real

for x, y being Point of (TOP-REAL n) holds

( y in Sphere (x,r) iff |.(y - x).| = r )

for r being Real

for x, y being Point of (TOP-REAL n) holds

( y in Sphere (x,r) iff |.(y - x).| = r )

proof end;

theorem :: TOPREAL9:10

for n being Nat

for r being Real

for y being Point of (TOP-REAL n) st y in Ball ((0. (TOP-REAL n)),r) holds

|.y.| < r

for r being Real

for y being Point of (TOP-REAL n) st y in Ball ((0. (TOP-REAL n)),r) holds

|.y.| < r

proof end;

theorem :: TOPREAL9:11

for n being Nat

for r being Real

for y being Point of (TOP-REAL n) st y in cl_Ball ((0. (TOP-REAL n)),r) holds

|.y.| <= r

for r being Real

for y being Point of (TOP-REAL n) st y in cl_Ball ((0. (TOP-REAL n)),r) holds

|.y.| <= r

proof end;

theorem :: TOPREAL9:12

for n being Nat

for r being Real

for y being Point of (TOP-REAL n) st y in Sphere ((0. (TOP-REAL n)),r) holds

|.y.| = r

for r being Real

for y being Point of (TOP-REAL n) st y in Sphere ((0. (TOP-REAL n)),r) holds

|.y.| = r

proof end;

theorem Th11: :: TOPREAL9:13

for n being Nat

for r being Real

for x being Point of (TOP-REAL n)

for e being Point of (Euclid n) st x = e holds

Ball (e,r) = Ball (x,r)

for r being Real

for x being Point of (TOP-REAL n)

for e being Point of (Euclid n) st x = e holds

Ball (e,r) = Ball (x,r)

proof end;

theorem Th12: :: TOPREAL9:14

for n being Nat

for r being Real

for x being Point of (TOP-REAL n)

for e being Point of (Euclid n) st x = e holds

cl_Ball (e,r) = cl_Ball (x,r)

for r being Real

for x being Point of (TOP-REAL n)

for e being Point of (Euclid n) st x = e holds

cl_Ball (e,r) = cl_Ball (x,r)

proof end;

theorem Th13: :: TOPREAL9:15

for n being Nat

for r being Real

for x being Point of (TOP-REAL n)

for e being Point of (Euclid n) st x = e holds

Sphere (e,r) = Sphere (x,r)

for r being Real

for x being Point of (TOP-REAL n)

for e being Point of (Euclid n) st x = e holds

Sphere (e,r) = Sphere (x,r)

proof end;

theorem :: TOPREAL9:16

for n being Nat

for r being Real

for x being Point of (TOP-REAL n) holds Ball (x,r) c= cl_Ball (x,r)

for r being Real

for x being Point of (TOP-REAL n) holds Ball (x,r) c= cl_Ball (x,r)

proof end;

theorem Th15: :: TOPREAL9:17

for n being Nat

for r being Real

for x being Point of (TOP-REAL n) holds Sphere (x,r) c= cl_Ball (x,r)

for r being Real

for x being Point of (TOP-REAL n) holds Sphere (x,r) c= cl_Ball (x,r)

proof end;

theorem Th16: :: TOPREAL9:18

for n being Nat

for r being Real

for x being Point of (TOP-REAL n) holds (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r)

for r being Real

for x being Point of (TOP-REAL n) holds (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r)

proof end;

theorem Th17: :: TOPREAL9:19

for n being Nat

for r being Real

for x being Point of (TOP-REAL n) holds Ball (x,r) misses Sphere (x,r)

for r being Real

for x being Point of (TOP-REAL n) holds Ball (x,r) misses Sphere (x,r)

proof end;

registration

let n be Nat;

let x be Point of (TOP-REAL n);

let r be non positive Real;

coherence

Ball (x,r) is empty

end;
let x be Point of (TOP-REAL n);

let r be non positive Real;

coherence

Ball (x,r) is empty

proof end;

registration

let n be Nat;

let x be Point of (TOP-REAL n);

let r be positive Real;

coherence

not Ball (x,r) is empty

end;
let x be Point of (TOP-REAL n);

let r be positive Real;

coherence

not Ball (x,r) is empty

proof end;

theorem :: TOPREAL9:20

theorem :: TOPREAL9:21

registration

let n be Nat;

let x be Point of (TOP-REAL n);

let r be negative Real;

coherence

cl_Ball (x,r) is empty

end;
let x be Point of (TOP-REAL n);

let r be negative Real;

coherence

cl_Ball (x,r) is empty

proof end;

registration

let n be Nat;

let x be Point of (TOP-REAL n);

let r be non negative Real;

coherence

not cl_Ball (x,r) is empty

end;
let x be Point of (TOP-REAL n);

let r be non negative Real;

coherence

not cl_Ball (x,r) is empty

proof end;

theorem :: TOPREAL9:22

theorem :: TOPREAL9:23

theorem Th22: :: TOPREAL9:24

for n being Nat

for a, b, r being Real

for x, y, z being Point of (TOP-REAL n) st a + b = 1 & |.a.| + |.b.| = 1 & b <> 0 & x in cl_Ball (z,r) & y in Ball (z,r) holds

(a * x) + (b * y) in Ball (z,r)

for a, b, r being Real

for x, y, z being Point of (TOP-REAL n) st a + b = 1 & |.a.| + |.b.| = 1 & b <> 0 & x in cl_Ball (z,r) & y in Ball (z,r) holds

(a * x) + (b * y) in Ball (z,r)

proof end;

registration

let n be Nat;

let x be Point of (TOP-REAL n);

let r be Real;

coherence

Ball (x,r) is open

cl_Ball (x,r) is closed

Sphere (x,r) is closed

end;
let x be Point of (TOP-REAL n);

let r be Real;

coherence

Ball (x,r) is open

proof end;

coherence cl_Ball (x,r) is closed

proof end;

coherence Sphere (x,r) is closed

proof end;

registration

let n be Nat;

let x be Point of (TOP-REAL n);

let r be Real;

coherence

Ball (x,r) is bounded

cl_Ball (x,r) is bounded

Sphere (x,r) is bounded

end;
let x be Point of (TOP-REAL n);

let r be Real;

coherence

Ball (x,r) is bounded

proof end;

coherence cl_Ball (x,r) is bounded

proof end;

coherence Sphere (x,r) is bounded

proof end;

Lm1: for n being Nat

for a being Real

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

proof end;

Lm2: for n being Nat

for a being Real

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

proof end;

:: Convex subsets of TOP-REAL n

registration

let n be Nat;

let x be Point of (TOP-REAL n);

let r be Real;

coherence

Ball (x,r) is convex by Lm2;

coherence

cl_Ball (x,r) is convex by Lm1;

end;
let x be Point of (TOP-REAL n);

let r be Real;

coherence

Ball (x,r) is convex by Lm2;

coherence

cl_Ball (x,r) is convex by Lm1;

:: 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

for x being Point of (TOP-REAL n) holds f . (r * x) = r * (f . x) );

for n being Nat

for f being Function of (TOP-REAL n),(TOP-REAL n) holds

( f is homogeneous iff for r being Real

for x being Point of (TOP-REAL n) holds f . (r * x) = r * (f . x) );

registration

let n be Nat;

coherence

( (TOP-REAL n) --> (0. (TOP-REAL n)) is homogeneous & (TOP-REAL n) --> (0. (TOP-REAL n)) is additive )

end;
coherence

( (TOP-REAL n) --> (0. (TOP-REAL n)) is homogeneous & (TOP-REAL n) --> (0. (TOP-REAL n)) is additive )

proof end;

registration

let n be Nat;

ex b_{1} being Function of (TOP-REAL n),(TOP-REAL n) st

( b_{1} is homogeneous & b_{1} is additive & b_{1} is continuous )

end;
cluster V1() V21() V30( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)) continuous additive homogeneous for Function of ,;

existence ex b

( b

proof end;

registration

let a, c be Real;

coherence

( AffineMap (a,0,c,0) is homogeneous & AffineMap (a,0,c,0) is additive )

end;
coherence

( AffineMap (a,0,c,0) is homogeneous & AffineMap (a,0,c,0) is additive )

proof end;

theorem :: TOPREAL9:25

for n being Nat

for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n)

for X being convex Subset of (TOP-REAL n) holds f .: X is convex

for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n)

for X being convex Subset of (TOP-REAL n) holds f .: X is convex

proof end;

definition

let V be RealLinearSpace;

let p, q be Element of V;

{ (((1 - l) * p) + (l * q)) where l is Real : 0 <= l } is Subset of V

end;
let p, q be Element of V;

func halfline (p,q) -> Subset of V equals :: TOPREAL9:def 5

{ (((1 - l) * p) + (l * q)) where l is Real : 0 <= l } ;

coherence { (((1 - l) * p) + (l * q)) where l is Real : 0 <= l } ;

{ (((1 - l) * p) + (l * q)) where l is Real : 0 <= l } is Subset of V

proof end;

:: deftheorem defines halfline TOPREAL9:def 5 :

for V being RealLinearSpace

for p, q being Element of V holds halfline (p,q) = { (((1 - l) * p) + (l * q)) where l is Real : 0 <= l } ;

for V being RealLinearSpace

for p, q being Element of V holds halfline (p,q) = { (((1 - l) * p) + (l * q)) where l is Real : 0 <= l } ;

theorem :: TOPREAL9:26

registration
end;

theorem Th28: :: TOPREAL9:30

for V being RealLinearSpace

for p, q, x being Element of V st x in halfline (p,q) holds

halfline (p,x) c= halfline (p,q)

for p, q, x being Element of V st x in halfline (p,q) holds

halfline (p,x) c= halfline (p,q)

proof end;

theorem :: TOPREAL9:31

for V being RealLinearSpace

for p, q, x being Element of V st x in halfline (p,q) & x <> p holds

halfline (p,q) = halfline (p,x)

for p, q, x being Element of V st x in halfline (p,q) & x <> p holds

halfline (p,q) = halfline (p,x)

proof end;

registration
end;

theorem Th31: :: TOPREAL9:33

for n being Nat

for r being Real

for y, z, x being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Ball (x,r) holds

(LSeg (y,z)) /\ (Sphere (x,r)) = {y}

for r being Real

for y, z, x being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Ball (x,r) holds

(LSeg (y,z)) /\ (Sphere (x,r)) = {y}

proof end;

theorem Th32: :: TOPREAL9:34

for n being Nat

for r being Real

for y, z, x being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Sphere (x,r) holds

(LSeg (y,z)) \ {y,z} c= Ball (x,r)

for r being Real

for y, z, x being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Sphere (x,r) holds

(LSeg (y,z)) \ {y,z} c= Ball (x,r)

proof end;

theorem Th33: :: TOPREAL9:35

for n being Nat

for r being Real

for y, z, x being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Sphere (x,r) holds

(LSeg (y,z)) /\ (Sphere (x,r)) = {y,z}

for r being Real

for y, z, x being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Sphere (x,r) holds

(LSeg (y,z)) /\ (Sphere (x,r)) = {y,z}

proof end;

theorem Th34: :: TOPREAL9:36

for n being Nat

for r being Real

for y, z, x being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Sphere (x,r) holds

(halfline (y,z)) /\ (Sphere (x,r)) = {y,z}

for r being Real

for y, z, x being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Sphere (x,r) holds

(halfline (y,z)) /\ (Sphere (x,r)) = {y,z}

proof end;

theorem Th35: :: TOPREAL9:37

for n being Nat

for a, r being Real

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) )

for a, r being Real

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) )

proof end;

theorem Th36: :: TOPREAL9:38

for n being Nat

for a, r being Real

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) ) )

for a, r being Real

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) ) )

proof end;

registration

let n be Nat;

let x be Point of (TOP-REAL n);

let r be negative Real;

coherence

Sphere (x,r) is empty

end;
let x be Point of (TOP-REAL n);

let r be negative Real;

coherence

Sphere (x,r) is empty

proof end;

registration

let n be non zero Nat;

let x be Point of (TOP-REAL n);

let r be non negative Real;

coherence

not Sphere (x,r) is empty

end;
let x be Point of (TOP-REAL n);

let r be non negative Real;

coherence

not Sphere (x,r) is empty

proof end;

theorem :: TOPREAL9:39

theorem :: TOPREAL9:40

theorem :: TOPREAL9:41

for a, b being Real

for s, t being Point of (TOP-REAL 2) holds ((a * s) + (b * t)) `1 = (a * (s `1)) + (b * (t `1))

for s, t being Point of (TOP-REAL 2) holds ((a * s) + (b * t)) `1 = (a * (s `1)) + (b * (t `1))

proof end;

theorem :: TOPREAL9:42

for a, b being Real

for s, t being Point of (TOP-REAL 2) holds ((a * s) + (b * t)) `2 = (a * (s `2)) + (b * (t `2))

for s, t being Point of (TOP-REAL 2) holds ((a * s) + (b * t)) `2 = (a * (s `2)) + (b * (t `2))

proof end;

theorem Th41: :: TOPREAL9:43

for a, b, r being Real

for t being Point of (TOP-REAL 2) holds

( t in circle (a,b,r) iff |.(t - |[a,b]|).| = r )

for t being Point of (TOP-REAL 2) holds

( t in circle (a,b,r) iff |.(t - |[a,b]|).| = r )

proof end;

theorem Th42: :: TOPREAL9:44

for a, b, r being Real

for t being Point of (TOP-REAL 2) holds

( t in closed_inside_of_circle (a,b,r) iff |.(t - |[a,b]|).| <= r )

for t being Point of (TOP-REAL 2) holds

( t in closed_inside_of_circle (a,b,r) iff |.(t - |[a,b]|).| <= r )

proof end;

theorem Th43: :: TOPREAL9:45

for a, b, r being Real

for t being Point of (TOP-REAL 2) holds

( t in inside_of_circle (a,b,r) iff |.(t - |[a,b]|).| < r )

for t being Point of (TOP-REAL 2) holds

( t in inside_of_circle (a,b,r) iff |.(t - |[a,b]|).| < r )

proof end;

registration
end;

registration

let a, b be Real;

let r be non negative Real;

coherence

not closed_inside_of_circle (a,b,r) is empty

end;
let r be non negative Real;

coherence

not closed_inside_of_circle (a,b,r) is empty

proof end;

theorem Th45: :: TOPREAL9:47

for a, b, r being Real

for x being Point of (Euclid 2) st x = |[a,b]| holds

cl_Ball (x,r) = closed_inside_of_circle (a,b,r)

for x being Point of (Euclid 2) st x = |[a,b]| holds

cl_Ball (x,r) = closed_inside_of_circle (a,b,r)

proof end;

theorem Th46: :: TOPREAL9:48

for a, b, r being Real

for x being Point of (Euclid 2) st x = |[a,b]| holds

Ball (x,r) = inside_of_circle (a,b,r)

for x being Point of (Euclid 2) st x = |[a,b]| holds

Ball (x,r) = inside_of_circle (a,b,r)

proof end;

theorem Th47: :: TOPREAL9:49

for a, b, r being Real

for x being Point of (Euclid 2) st x = |[a,b]| holds

Sphere (x,r) = circle (a,b,r)

for x being Point of (Euclid 2) st x = |[a,b]| holds

Sphere (x,r) = circle (a,b,r)

proof end;

theorem :: TOPREAL9:55

for a, b, r being Real holds (inside_of_circle (a,b,r)) \/ (circle (a,b,r)) = closed_inside_of_circle (a,b,r)

proof end;

theorem :: TOPREAL9:56

for r being Real

for s being Point of (TOP-REAL 2) st s in Sphere ((0. (TOP-REAL 2)),r) holds

((s `1) ^2) + ((s `2) ^2) = r ^2

for s being Point of (TOP-REAL 2) st s in Sphere ((0. (TOP-REAL 2)),r) holds

((s `1) ^2) + ((s `2) ^2) = r ^2

proof end;

theorem :: TOPREAL9:57

for a, b, r being Real

for s, t being Point of (TOP-REAL 2) st s <> t & s in closed_inside_of_circle (a,b,r) & t in closed_inside_of_circle (a,b,r) holds

r > 0

for s, t being Point of (TOP-REAL 2) st s <> t & s in closed_inside_of_circle (a,b,r) & t in closed_inside_of_circle (a,b,r) holds

r > 0

proof end;

theorem :: TOPREAL9:58

for a, b, r, w being Real

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) )

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) )

proof end;

theorem :: TOPREAL9:59

for a, b, r being Real

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}

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}

proof end;

theorem :: TOPREAL9:60

for a, b, r being Real

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)

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)

proof end;

theorem :: TOPREAL9:61

for a, b, r being Real

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}

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}

proof end;

theorem :: TOPREAL9:62

for a, b, r being Real

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}

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}

proof end;

theorem :: TOPREAL9:63

for a, b, r, w being Real

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) ) )

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) ) )

proof end;

registration

let a, b, r be Real;

coherence

inside_of_circle (a,b,r) is convex

closed_inside_of_circle (a,b,r) is convex

end;
coherence

inside_of_circle (a,b,r) is convex

proof end;

coherence closed_inside_of_circle (a,b,r) is convex

proof end;

:: 12.11.18 A.T.

theorem Th63: :: TOPREAL9:65

for V being RealLinearSpace

for p1, p2 being Point of V holds Line (p1,p2) = (halfline (p1,p2)) \/ (halfline (p2,p1))

for p1, p2 being Point of V holds Line (p1,p2) = (halfline (p1,p2)) \/ (halfline (p2,p1))

proof end;

theorem Th64: :: TOPREAL9:66

for V being RealLinearSpace

for p1, p2, p3 being Point of V holds

( not p1 in halfline (p2,p3) or p1 in LSeg (p2,p3) or p3 in LSeg (p2,p1) )

for p1, p2, p3 being Point of V holds

( not p1 in halfline (p2,p3) or p1 in LSeg (p2,p3) or p3 in LSeg (p2,p1) )

proof end;

theorem :: TOPREAL9:67

for V being RealLinearSpace

for p1, p2, p3 being Point of V holds

( p1,p2,p3 are_collinear iff ( p1 in LSeg (p2,p3) or p2 in LSeg (p3,p1) or p3 in LSeg (p1,p2) ) )

for p1, p2, p3 being Point of V holds

( p1,p2,p3 are_collinear iff ( p1 in LSeg (p2,p3) or p2 in LSeg (p3,p1) or p3 in LSeg (p1,p2) ) )

proof end;