:: Intersections of Intervals and Balls in TOP-REAL n
:: by Artur Korni{\l}owicz and Yasunari Shidama
::
:: Copyright (c) 2004-2019 Association of Mizar Users

theorem :: TOPREAL9:1
canceled;

theorem :: TOPREAL9:2
canceled;

::\$CT 2
theorem Th1: :: TOPREAL9:3
for n being Nat
for x being Point of () st not n is zero holds
x <> x + ()
proof end;

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 ) )
proof end;

theorem Th3: :: TOPREAL9:5
for f being real-valued FinSequence holds |.f.| ^2 = Sum (sqr f)
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
proof end;

definition
let n be Nat;
let x be Point of ();
let r be Real;
func Ball (x,r) -> Subset of () equals :: TOPREAL9:def 1
{ p where p is Point of () : |.(p - x).| < r } ;
coherence
{ p where p is Point of () : |.(p - x).| < r } is Subset of ()
proof end;
func cl_Ball (x,r) -> Subset of () equals :: TOPREAL9:def 2
{ p where p is Point of () : |.(p - x).| <= r } ;
coherence
{ p where p is Point of () : |.(p - x).| <= r } is Subset of ()
proof end;
func Sphere (x,r) -> Subset of () equals :: TOPREAL9:def 3
{ p where p is Point of () : |.(p - x).| = r } ;
coherence
{ p where p is Point of () : |.(p - x).| = r } is Subset of ()
proof end;
end;

:: deftheorem defines Ball TOPREAL9:def 1 :
for n being Nat
for x being Point of ()
for r being Real holds Ball (x,r) = { p where p is Point of () : |.(p - x).| < r } ;

:: deftheorem defines cl_Ball TOPREAL9:def 2 :
for n being Nat
for x being Point of ()
for r being Real holds cl_Ball (x,r) = { p where p is Point of () : |.(p - x).| <= r } ;

:: deftheorem defines Sphere TOPREAL9:def 3 :
for n being Nat
for x being Point of ()
for r being Real holds Sphere (x,r) = { p where p is Point of () : |.(p - x).| = r } ;

theorem Th5: :: TOPREAL9:7
for n being Nat
for r being Real
for x, y being Point of () 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 () 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 () 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 () st y in Ball ((0. ()),r) holds
|.y.| < r
proof end;

theorem :: TOPREAL9:11
for n being Nat
for r being Real
for y being Point of () st y in cl_Ball ((0. ()),r) holds
|.y.| <= r
proof end;

theorem :: TOPREAL9:12
for n being Nat
for r being Real
for y being Point of () st y in Sphere ((0. ()),r) holds
|.y.| = r
proof end;

theorem Th11: :: TOPREAL9:13
for n being Nat
for r being Real
for x being Point of ()
for e being Point of () 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 ()
for e being Point of () 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 ()
for e being Point of () 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 () 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 () 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 () 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 () holds Ball (x,r) misses Sphere (x,r)
proof end;

registration
let n be Nat;
let x be Point of ();
let r be non positive Real;
cluster Ball (x,r) -> empty ;
coherence
Ball (x,r) is empty
proof end;
end;

registration
let n be Nat;
let x be Point of ();
let r be positive Real;
cluster Ball (x,r) -> non empty ;
coherence
not Ball (x,r) is empty
proof end;
end;

theorem :: TOPREAL9:20
for n being Nat
for r being Real
for x being Point of () st not Ball (x,r) is empty holds
r > 0 ;

theorem :: TOPREAL9:21
for n being Nat
for r being Real
for x being Point of () st Ball (x,r) is empty holds
r <= 0 ;

registration
let n be Nat;
let x be Point of ();
let r be negative Real;
cluster cl_Ball (x,r) -> empty ;
coherence
cl_Ball (x,r) is empty
proof end;
end;

registration
let n be Nat;
let x be Point of ();
let r be non negative Real;
cluster cl_Ball (x,r) -> non empty ;
coherence
not cl_Ball (x,r) is empty
proof end;
end;

theorem :: TOPREAL9:22
for n being Nat
for r being Real
for x being Point of () st not cl_Ball (x,r) is empty holds
r >= 0 ;

theorem :: TOPREAL9:23
for n being Nat
for r being Real
for x being Point of () st cl_Ball (x,r) is empty holds
r < 0 ;

theorem Th22: :: TOPREAL9:24
for n being Nat
for a, b, r being Real
for x, y, z being Point of () 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 ();
let r be Real;
cluster Ball (x,r) -> open ;
coherence
Ball (x,r) is open
proof end;
cluster cl_Ball (x,r) -> closed ;
coherence
cl_Ball (x,r) is closed
proof end;
cluster Sphere (x,r) -> closed ;
coherence
Sphere (x,r) is closed
proof end;
end;

registration
let n be Nat;
let x be Point of ();
let r be Real;
cluster Ball (x,r) -> bounded ;
coherence
Ball (x,r) is bounded
proof end;
cluster cl_Ball (x,r) -> bounded ;
coherence
cl_Ball (x,r) is bounded
proof end;
cluster Sphere (x,r) -> bounded ;
coherence
Sphere (x,r) is bounded
proof end;
end;

Lm1: for n being Nat
for a being Real
for P being Subset of ()
for Q being Point of () st P = { q where q is Point of () : |.(q - Q).| <= a } holds
P is convex

proof end;

Lm2: for n being Nat
for a being Real
for P being Subset of ()
for Q being Point of () st P = { q where q is Point of () : |.(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 ();
let r be Real;
cluster Ball (x,r) -> convex ;
coherence
Ball (x,r) is convex
by Lm2;
cluster cl_Ball (x,r) -> convex ;
coherence
cl_Ball (x,r) is convex
by Lm1;
end;

definition
let n be Nat;
let f be Function of (),();
attr f is homogeneous means :Def4: :: TOPREAL9:def 4
for r being Real
for x being Point of () holds f . (r * x) = r * (f . x);
end;

:: deftheorem Def4 defines homogeneous TOPREAL9:def 4 :
for n being Nat
for f being Function of (),() holds
( f is homogeneous iff for r being Real
for x being Point of () holds f . (r * x) = r * (f . x) );

registration
let n be Nat;
cluster () --> (0. ()) -> additive homogeneous ;
coherence
( () --> (0. ()) is homogeneous & () --> (0. ()) is additive )
proof end;
end;

registration
let n be Nat;
cluster V1() V21() V30( the carrier of (), the carrier of ()) continuous additive homogeneous for Element of K16(K17( the carrier of (), the carrier of ()));
existence
ex b1 being Function of (),() st
( b1 is homogeneous & b1 is additive & b1 is continuous )
proof end;
end;

registration
let a, c be Real;
cluster AffineMap (a,0,c,0) -> additive homogeneous ;
coherence
( AffineMap (a,0,c,0) is homogeneous & AffineMap (a,0,c,0) is additive )
proof end;
end;

theorem :: TOPREAL9:25
for n being Nat
for f being additive homogeneous Function of (),()
for X being convex Subset of () holds f .: X is convex
proof end;

definition
let V be RealLinearSpace;
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 } is Subset of V
proof end;
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 } ;

theorem :: TOPREAL9:26
for V being RealLinearSpace
for p, q being Element of V
for x being set holds
( x in halfline (p,q) iff ex l being Real st
( x = ((1 - l) * p) + (l * q) & 0 <= l ) ) ;

registration
let V be RealLinearSpace;
let p, q be Element of V;
cluster halfline (p,q) -> non empty ;
coherence
not halfline (p,q) is empty
proof end;
end;

theorem Th25: :: TOPREAL9:27
for V being RealLinearSpace
for p, q being Element of V holds p in halfline (p,q)
proof end;

theorem Th26: :: TOPREAL9:28
for V being RealLinearSpace
for p, q being Element of V holds q in halfline (p,q)
proof end;

theorem Th27: :: TOPREAL9:29
for V being RealLinearSpace
for p being Element of V holds halfline (p,p) = {p}
proof 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)
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)
proof end;

theorem :: TOPREAL9:32
for V being RealLinearSpace
for p, q being Element of V holds LSeg (p,q) c= halfline (p,q)
proof end;

registration
let V be RealLinearSpace;
let p, q be Element of V;
cluster halfline (p,q) -> convex ;
coherence
halfline (p,q) is convex
proof end;
end;

theorem Th31: :: TOPREAL9:33
for n being Nat
for r being Real
for y, z, x being Point of () 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 () 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 () 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 () 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 ()
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 () 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 ()
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 () 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 ();
let r be negative Real;
cluster Sphere (x,r) -> empty ;
coherence
Sphere (x,r) is empty
proof end;
end;

registration
let n be non zero Nat;
let x be Point of ();
let r be non negative Real;
cluster Sphere (x,r) -> non empty ;
coherence
not Sphere (x,r) is empty
proof end;
end;

theorem :: TOPREAL9:39
for n being Nat
for r being Real
for x being Point of () st not Sphere (x,r) is empty holds
r >= 0 ;

theorem :: TOPREAL9:40
for n being Nat
for r being Real
for x being Point of () st not n is zero & Sphere (x,r) is empty holds
r < 0 ;

theorem :: TOPREAL9:41
for a, b being Real
for s, t being Point of () 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 () 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 () 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 () 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 () holds
( t in inside_of_circle (a,b,r) iff |.(t - |[a,b]|).| < r )
proof end;

registration
let a, b be Real;
let r be positive Real;
cluster inside_of_circle (a,b,r) -> non empty ;
coherence
not inside_of_circle (a,b,r) is empty
proof end;
end;

registration
let a, b be Real;
let r be non negative Real;
cluster closed_inside_of_circle (a,b,r) -> non empty ;
coherence
not closed_inside_of_circle (a,b,r) is empty
proof end;
end;

theorem :: TOPREAL9:46
for a, b, r being Real holds circle (a,b,r) c= closed_inside_of_circle (a,b,r)
proof end;

theorem Th45: :: TOPREAL9:47
for a, b, r being Real
for x being Point of () 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 () 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 () st x = |[a,b]| holds
Sphere (x,r) = circle (a,b,r)
proof end;

theorem Th48: :: TOPREAL9:50
for a, b, r being Real holds Ball (|[a,b]|,r) = inside_of_circle (a,b,r)
proof end;

theorem :: TOPREAL9:51
for a, b, r being Real holds cl_Ball (|[a,b]|,r) = closed_inside_of_circle (a,b,r)
proof end;

theorem Th50: :: TOPREAL9:52
for a, b, r being Real holds Sphere (|[a,b]|,r) = circle (a,b,r)
proof end;

theorem :: TOPREAL9:53
for a, b, r being Real holds inside_of_circle (a,b,r) c= closed_inside_of_circle (a,b,r)
proof end;

theorem :: TOPREAL9:54
for a, b, r being Real holds inside_of_circle (a,b,r) misses 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 () st s in Sphere ((0. ()),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 () 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 ()
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 () 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 () 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 () 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 () 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 () 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 ()
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 () 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;
cluster inside_of_circle (a,b,r) -> convex ;
coherence
inside_of_circle (a,b,r) is convex
proof end;
cluster closed_inside_of_circle (a,b,r) -> convex ;
coherence
closed_inside_of_circle (a,b,r) is convex
proof end;
end;

:: 12.11.18 A.T.
theorem Th62: :: TOPREAL9:64
for V being RealLinearSpace
for p1, p2 being Point of V holds halfline (p1,p2) c= Line (p1,p2)
proof end;

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))
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) )
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) ) )
proof end;