topreal9.miz
begin
reserve n for
Nat,
a,b,r,w for
Real,
x,y,z for
Point of (
TOP-REAL n),
e for
Point of (
Euclid n);
::$Canceled
theorem ::
TOPREAL9:3
Th1: n is non
zero implies x
<> (x
+ (
1.REAL n))
proof
A1: (
0.REAL n)
= (
0. (
TOP-REAL n)) & x
= (x
+ (
0. (
TOP-REAL n))) by
EUCLID: 66,
RLVECT_1: 4;
assume that
A2: n is non
zero and
A3: x
= (x
+ (
1.REAL n));
(
0.REAL n)
<> (
1.REAL n) by
A2,
REVROT_1: 19;
hence thesis by
A1,
A3,
RLVECT_1: 8;
end;
theorem ::
TOPREAL9:4
Th2: for V be
RealLinearSpace, y,z be
Point of V holds for x be
object holds x
= (((1
- r)
* y)
+ (r
* z)) implies (x
= y iff r
=
0 or y
= z) & (x
= z iff r
= 1 or y
= z)
proof
let V be
RealLinearSpace, y,z be
Point of V;
let x be
object;
assume
A1: x
= (((1
- r)
* y)
+ (r
* z));
hereby
assume x
= y;
then (
0. V)
= ((((1
- r)
* y)
+ (r
* z))
- y) by
A1,
RLVECT_1: 5
.= ((((1
- r)
* y)
- y)
+ (r
* z)) by
RLVECT_1:def 3
.= ((((1
- r)
* y)
- (1
* y))
+ (r
* z)) by
RLVECT_1:def 8
.= ((((1
- r)
- 1)
* y)
+ (r
* z)) by
RLVECT_1: 35
.= ((r
* z)
- (r
* y)) by
RLVECT_1: 79
.= (r
* (z
- y)) by
RLVECT_1: 34;
then r
=
0 or (z
- y)
= (
0. V) by
RLVECT_1: 11;
hence r
=
0 or y
= z by
RLVECT_1: 21;
end;
hereby
assume
A2: r
=
0 or y
= z;
per cases by
A2;
suppose r
=
0 ;
hence x
= (y
+ (
0
* z)) by
A1,
RLVECT_1:def 8
.= (y
+ (
0. V)) by
RLVECT_1: 10
.= y by
RLVECT_1: 4;
end;
suppose z
= y;
hence x
= (((1
- r)
+ r)
* y) by
A1,
RLVECT_1:def 6
.= y by
RLVECT_1:def 8;
end;
end;
hereby
assume x
= z;
then (
0. V)
= ((((1
- r)
* y)
+ (r
* z))
- z) by
A1,
RLVECT_1: 5
.= (((1
- r)
* y)
+ ((r
* z)
- z)) by
RLVECT_1:def 3
.= (((1
- r)
* y)
+ ((r
* z)
+ ((
- 1)
* z))) by
RLVECT_1: 16
.= (((1
- r)
* y)
+ (((
- 1)
+ r)
* z)) by
RLVECT_1:def 6
.= (((1
- r)
* y)
+ ((
- (1
- r))
* z))
.= (((1
- r)
* y)
- ((1
- r)
* z)) by
RLVECT_1: 79
.= ((1
- r)
* (y
- z)) by
RLVECT_1: 34;
then ((1
- r)
+ r)
= (
0
+ r) or (y
- z)
= (
0. V) by
RLVECT_1: 11;
hence r
= 1 or y
= z by
RLVECT_1: 21;
end;
assume
A3: r
= 1 or y
= z;
per cases by
A3;
suppose r
= 1;
hence x
= ((
0. V)
+ (1
* z)) by
A1,
RLVECT_1: 10
.= (1
* z) by
RLVECT_1: 4
.= z by
RLVECT_1:def 8;
end;
suppose y
= z;
hence x
= (((1
- r)
+ r)
* z) by
A1,
RLVECT_1:def 6
.= z by
RLVECT_1:def 8;
end;
end;
theorem ::
TOPREAL9:5
Th3: for f be
real-valued
FinSequence holds (
|.f.|
^2 )
= (
Sum (
sqr f))
proof
let f be
real-valued
FinSequence;
(
Sum (
sqr f))
>=
0 by
RVSUM_1: 86;
hence thesis by
SQUARE_1:def 2;
end;
theorem ::
TOPREAL9:6
Th4: for M be non
empty
MetrSpace, z1,z2,z3 be
Point of M st z1
<> z2 & z1
in (
cl_Ball (z3,r)) & z2
in (
cl_Ball (z3,r)) holds r
>
0
proof
let M be non
empty
MetrSpace, z1,z2,z3 be
Point of M such that
A1: z1
<> z2 and
A2: z1
in (
cl_Ball (z3,r)) and
A3: z2
in (
cl_Ball (z3,r));
now
assume r
=
0 ;
then
A4: (
cl_Ball (z3,r))
=
{z3} by
TOPREAL6: 56;
then z1
= z3 by
A2,
TARSKI:def 1;
hence contradiction by
A1,
A3,
A4,
TARSKI:def 1;
end;
hence thesis by
A2,
TOPREAL6: 55;
end;
begin
definition
let n be
Nat, x be
Point of (
TOP-REAL n), r be
Real;
::
TOPREAL9:def1
func
Ball (x,r) ->
Subset of (
TOP-REAL n) equals { p where p be
Point of (
TOP-REAL n) :
|.(p
- x).|
< r };
coherence
proof
{ p where p be
Point of (
TOP-REAL n) :
|.(p
- x).|
< r }
c= the
carrier of (
TOP-REAL n)
proof
let q be
object;
assume q
in { p where p be
Point of (
TOP-REAL n) :
|.(p
- x).|
< r };
then ex p be
Point of (
TOP-REAL n) st q
= p &
|.(p
- x).|
< r;
hence thesis;
end;
hence thesis;
end;
::
TOPREAL9:def2
func
cl_Ball (x,r) ->
Subset of (
TOP-REAL n) equals { p where p be
Point of (
TOP-REAL n) :
|.(p
- x).|
<= r };
coherence
proof
{ p where p be
Point of (
TOP-REAL n) :
|.(p
- x).|
<= r }
c= the
carrier of (
TOP-REAL n)
proof
let q be
object;
assume q
in { p where p be
Point of (
TOP-REAL n) :
|.(p
- x).|
<= r };
then ex p be
Point of (
TOP-REAL n) st q
= p &
|.(p
- x).|
<= r;
hence thesis;
end;
hence thesis;
end;
::
TOPREAL9:def3
func
Sphere (x,r) ->
Subset of (
TOP-REAL n) equals { p where p be
Point of (
TOP-REAL n) :
|.(p
- x).|
= r };
coherence
proof
{ p where p be
Point of (
TOP-REAL n) :
|.(p
- x).|
= r }
c= the
carrier of (
TOP-REAL n)
proof
let q be
object;
assume q
in { p where p be
Point of (
TOP-REAL n) :
|.(p
- x).|
= r };
then ex p be
Point of (
TOP-REAL n) st q
= p &
|.(p
- x).|
= r;
hence thesis;
end;
hence thesis;
end;
end
theorem ::
TOPREAL9:7
Th5: y
in (
Ball (x,r)) iff
|.(y
- x).|
< r
proof
hereby
assume y
in (
Ball (x,r));
then ex p be
Point of (
TOP-REAL n) st y
= p &
|.(p
- x).|
< r;
hence
|.(y
- x).|
< r;
end;
thus thesis;
end;
theorem ::
TOPREAL9:8
Th6: y
in (
cl_Ball (x,r)) iff
|.(y
- x).|
<= r
proof
hereby
assume y
in (
cl_Ball (x,r));
then ex p be
Point of (
TOP-REAL n) st y
= p &
|.(p
- x).|
<= r;
hence
|.(y
- x).|
<= r;
end;
thus thesis;
end;
theorem ::
TOPREAL9:9
Th7: y
in (
Sphere (x,r)) iff
|.(y
- x).|
= r
proof
hereby
assume y
in (
Sphere (x,r));
then ex p be
Point of (
TOP-REAL n) st y
= p &
|.(p
- x).|
= r;
hence
|.(y
- x).|
= r;
end;
thus thesis;
end;
theorem ::
TOPREAL9:10
y
in (
Ball ((
0. (
TOP-REAL n)),r)) implies
|.y.|
< r
proof
assume y
in (
Ball ((
0. (
TOP-REAL n)),r));
then
|.(y
- (
0. (
TOP-REAL n))).|
< r by
Th5;
hence thesis by
RLVECT_1: 13;
end;
theorem ::
TOPREAL9:11
y
in (
cl_Ball ((
0. (
TOP-REAL n)),r)) implies
|.y.|
<= r
proof
assume y
in (
cl_Ball ((
0. (
TOP-REAL n)),r));
then
|.(y
- (
0. (
TOP-REAL n))).|
<= r by
Th6;
hence thesis by
RLVECT_1: 13;
end;
theorem ::
TOPREAL9:12
y
in (
Sphere ((
0. (
TOP-REAL n)),r)) implies
|.y.|
= r
proof
assume y
in (
Sphere ((
0. (
TOP-REAL n)),r));
then
|.(y
- (
0. (
TOP-REAL n))).|
= r by
Th7;
hence thesis by
RLVECT_1: 13;
end;
theorem ::
TOPREAL9:13
Th11: x
= e implies (
Ball (e,r))
= (
Ball (x,r))
proof
assume
A1: x
= e;
hereby
let q be
object;
assume
A2: q
in (
Ball (e,r));
then
reconsider f = q as
Point of (
Euclid n);
reconsider p = f as
Point of (
TOP-REAL n) by
TOPREAL3: 8;
(
dist (f,e))
< r by
A2,
METRIC_1: 11;
then
|.(p
- x).|
< r by
A1,
JGRAPH_1: 28;
hence q
in (
Ball (x,r));
end;
let q be
object;
assume
A3: q
in (
Ball (x,r));
then
reconsider q as
Point of (
TOP-REAL n);
reconsider f = q as
Point of (
Euclid n) by
TOPREAL3: 8;
|.(q
- x).|
< r by
A3,
Th5;
then (
dist (f,e))
< r by
A1,
JGRAPH_1: 28;
hence thesis by
METRIC_1: 11;
end;
theorem ::
TOPREAL9:14
Th12: x
= e implies (
cl_Ball (e,r))
= (
cl_Ball (x,r))
proof
assume
A1: x
= e;
hereby
let q be
object;
assume
A2: q
in (
cl_Ball (e,r));
then
reconsider f = q as
Point of (
Euclid n);
reconsider p = f as
Point of (
TOP-REAL n) by
TOPREAL3: 8;
(
dist (f,e))
<= r by
A2,
METRIC_1: 12;
then
|.(p
- x).|
<= r by
A1,
JGRAPH_1: 28;
hence q
in (
cl_Ball (x,r));
end;
let q be
object;
assume
A3: q
in (
cl_Ball (x,r));
then
reconsider q as
Point of (
TOP-REAL n);
reconsider f = q as
Point of (
Euclid n) by
TOPREAL3: 8;
|.(q
- x).|
<= r by
A3,
Th6;
then (
dist (f,e))
<= r by
A1,
JGRAPH_1: 28;
hence thesis by
METRIC_1: 12;
end;
theorem ::
TOPREAL9:15
Th13: x
= e implies (
Sphere (e,r))
= (
Sphere (x,r))
proof
assume
A1: x
= e;
hereby
let q be
object;
assume
A2: q
in (
Sphere (e,r));
then
reconsider f = q as
Point of (
Euclid n);
reconsider p = f as
Point of (
TOP-REAL n) by
TOPREAL3: 8;
(
dist (f,e))
= r by
A2,
METRIC_1: 13;
then
|.(p
- x).|
= r by
A1,
JGRAPH_1: 28;
hence q
in (
Sphere (x,r));
end;
let q be
object;
assume
A3: q
in (
Sphere (x,r));
then
reconsider q as
Point of (
TOP-REAL n);
reconsider f = q as
Point of (
Euclid n) by
TOPREAL3: 8;
|.(q
- x).|
= r by
A3,
Th7;
then (
dist (f,e))
= r by
A1,
JGRAPH_1: 28;
hence thesis by
METRIC_1: 13;
end;
theorem ::
TOPREAL9:16
(
Ball (x,r))
c= (
cl_Ball (x,r))
proof
reconsider e = x as
Point of (
Euclid n) by
TOPREAL3: 8;
(
Ball (x,r))
= (
Ball (e,r)) & (
cl_Ball (x,r))
= (
cl_Ball (e,r)) by
Th11,
Th12;
hence thesis by
METRIC_1: 14;
end;
theorem ::
TOPREAL9:17
Th15: (
Sphere (x,r))
c= (
cl_Ball (x,r))
proof
reconsider e = x as
Point of (
Euclid n) by
TOPREAL3: 8;
(
Sphere (x,r))
= (
Sphere (e,r)) & (
cl_Ball (x,r))
= (
cl_Ball (e,r)) by
Th12,
Th13;
hence thesis by
METRIC_1: 15;
end;
theorem ::
TOPREAL9:18
Th16: ((
Ball (x,r))
\/ (
Sphere (x,r)))
= (
cl_Ball (x,r))
proof
reconsider e = x as
Point of (
Euclid n) by
TOPREAL3: 8;
A1: (
cl_Ball (x,r))
= (
cl_Ball (e,r)) by
Th12;
(
Sphere (x,r))
= (
Sphere (e,r)) & (
Ball (x,r))
= (
Ball (e,r)) by
Th11,
Th13;
hence thesis by
A1,
METRIC_1: 16;
end;
theorem ::
TOPREAL9:19
Th17: (
Ball (x,r))
misses (
Sphere (x,r))
proof
assume not thesis;
then
consider q be
object such that
A1: q
in (
Ball (x,r)) and
A2: q
in (
Sphere (x,r)) by
XBOOLE_0: 3;
reconsider q as
Point of (
TOP-REAL n) by
A1;
|.(q
- x).|
= r by
A2,
Th7;
hence thesis by
A1,
Th5;
end;
registration
let n be
Nat, x be
Point of (
TOP-REAL n);
let r be non
positive
Real;
cluster (
Ball (x,r)) ->
empty;
coherence
proof
assume not thesis;
then
consider y be
Point of (
TOP-REAL n) such that
A1: y
in (
Ball (x,r));
|.(y
- x).|
< r by
A1,
Th5;
hence contradiction;
end;
end
registration
let n be
Nat, x be
Point of (
TOP-REAL n);
let r be
positive
Real;
cluster (
Ball (x,r)) -> non
empty;
coherence
proof
reconsider e = x as
Point of (
Euclid n) by
TOPREAL3: 8;
(
Ball (x,r))
= (
Ball (e,r)) by
Th11;
hence thesis by
GOBOARD6: 1;
end;
end
theorem ::
TOPREAL9:20
(
Ball (x,r)) is non
empty implies r
>
0 ;
theorem ::
TOPREAL9:21
(
Ball (x,r)) is
empty implies r
<=
0 ;
registration
let n be
Nat, x be
Point of (
TOP-REAL n);
let r be
negative
Real;
cluster (
cl_Ball (x,r)) ->
empty;
coherence
proof
assume not thesis;
then
consider y be
Point of (
TOP-REAL n) such that
A1: y
in (
cl_Ball (x,r));
|.(y
- x).|
<= r by
A1,
Th6;
hence contradiction;
end;
end
registration
let n be
Nat, x be
Point of (
TOP-REAL n);
let r be non
negative
Real;
cluster (
cl_Ball (x,r)) -> non
empty;
coherence
proof
|.(x
- x).|
=
0 by
TOPRNS_1: 28;
hence thesis by
Th6;
end;
end
theorem ::
TOPREAL9:22
(
cl_Ball (x,r)) is non
empty implies r
>=
0 ;
theorem ::
TOPREAL9:23
(
cl_Ball (x,r)) is
empty implies r
<
0 ;
theorem ::
TOPREAL9:24
Th22: (a
+ b)
= 1 & (
|.a.|
+
|.b.|)
= 1 & b
<>
0 & x
in (
cl_Ball (z,r)) & y
in (
Ball (z,r)) implies ((a
* x)
+ (b
* y))
in (
Ball (z,r))
proof
assume that
A1: (a
+ b)
= 1 and
A2: (
|.a.|
+
|.b.|)
= 1 and
A3: b
<>
0 and
A4: x
in (
cl_Ball (z,r)) and
A5: y
in (
Ball (z,r));
|.(y
- z).|
< r by
A5,
Th5;
then
A6:
|.(z
- y).|
< r by
TOPRNS_1: 27;
|.(x
- z).|
<= r by
A4,
Th6;
then
0
<=
|.a.| &
|.(z
- x).|
<= r by
COMPLEX1: 46,
TOPRNS_1: 27;
then
A7: (
|.a.|
*
|.(z
- x).|)
<= (
|.a.|
* r) by
XREAL_1: 64;
0
<
|.b.| by
A3,
COMPLEX1: 47;
then (
|.b.|
*
|.(z
- y).|)
< (
|.b.|
* r) by
A6,
XREAL_1: 68;
then ((
|.a.|
*
|.(z
- x).|)
+ (
|.b.|
*
|.(z
- y).|))
< ((
|.a.|
* r)
+ (
|.b.|
* r)) by
A7,
XREAL_1: 8;
then a is
Real & ((
|.a.|
*
|.(z
- x).|)
+ (
|.b.|
*
|.(z
- y).|))
< ((
|.a.|
+
|.b.|)
* r);
then b is
Real & (
|.(a
* (z
- x)).|
+ (
|.b.|
*
|.(z
- y).|))
< (1
* r) by
A2,
TOPRNS_1: 7;
then
A8: (
|.(a
* (z
- x)).|
+
|.(b
* (z
- y)).|)
< r by
TOPRNS_1: 7;
|.(((a
* z)
+ (b
* z))
- ((a
* x)
+ (b
* y))).|
=
|.(((a
* z)
- ((a
* x)
+ (b
* y)))
+ (b
* z)).| by
RLVECT_1:def 3
.=
|.((((a
* z)
- (a
* x))
- (b
* y))
+ (b
* z)).| by
RLVECT_1: 27
.=
|.((((a
* z)
- (a
* x))
+ (b
* z))
- (b
* y)).| by
RLVECT_1:def 3
.=
|.(((a
* z)
- (a
* x))
+ ((b
* z)
- (b
* y))).| by
RLVECT_1:def 3
.=
|.((a
* (z
- x))
+ ((b
* z)
- (b
* y))).| by
RLVECT_1: 34
.=
|.((a
* (z
- x))
+ (b
* (z
- y))).| by
RLVECT_1: 34;
then
|.(((a
* z)
+ (b
* z))
- ((a
* x)
+ (b
* y))).|
<= (
|.(a
* (z
- x)).|
+
|.(b
* (z
- y)).|) by
TOPRNS_1: 29;
then
|.(((a
* z)
+ (b
* z))
- ((a
* x)
+ (b
* y))).|
< r by
A8,
XXREAL_0: 2;
then
A9:
|.(((a
* x)
+ (b
* y))
- ((a
* z)
+ (b
* z))).|
< r by
TOPRNS_1: 27;
((a
* z)
+ (b
* z))
= ((a
+ b)
* z) by
RLVECT_1:def 6
.= z by
A1,
RLVECT_1:def 8;
hence thesis by
A9;
end;
registration
let n be
Nat, x be
Point of (
TOP-REAL n);
let r;
cluster (
Ball (x,r)) ->
open;
coherence
proof
reconsider e = x as
Point of (
Euclid n) by
TOPREAL3: 8;
(
Ball (e,r))
= (
Ball (x,r)) by
Th11;
hence thesis by
GOBOARD6: 3;
end;
cluster (
cl_Ball (x,r)) ->
closed;
coherence
proof
reconsider e = x as
Point of (
Euclid n) by
TOPREAL3: 8;
(
cl_Ball (e,r)) is
bounded & (
cl_Ball (e,r))
= (
cl_Ball (x,r)) by
Th12,
TOPREAL6: 59;
hence thesis by
TOPREAL6: 58;
end;
cluster (
Sphere (x,r)) ->
closed;
coherence
proof
reconsider e = x as
Point of (
Euclid n) by
TOPREAL3: 8;
(
Sphere (e,r)) is
bounded & (
Sphere (e,r))
= (
Sphere (x,r)) by
Th13,
TOPREAL6: 62;
hence thesis by
TOPREAL6: 61;
end;
end
registration
let n, x, r;
cluster (
Ball (x,r)) ->
bounded;
coherence
proof
reconsider e = x as
Point of (
Euclid n) by
TOPREAL3: 8;
(
Ball (e,r))
= (
Ball (x,r)) by
Th11;
hence thesis by
JORDAN2C: 11;
end;
cluster (
cl_Ball (x,r)) ->
bounded;
coherence
proof
reconsider e = x as
Point of (
Euclid n) by
TOPREAL3: 8;
(
cl_Ball (e,r)) is
bounded & (
cl_Ball (e,r))
= (
cl_Ball (x,r)) by
Th12,
TOPREAL6: 59;
hence thesis by
JORDAN2C: 11;
end;
cluster (
Sphere (x,r)) ->
bounded;
coherence
proof
reconsider e = x as
Point of (
Euclid n) by
TOPREAL3: 8;
(
Sphere (e,r)) is
bounded & (
Sphere (e,r))
= (
Sphere (x,r)) by
Th13,
TOPREAL6: 62;
hence thesis by
JORDAN2C: 11;
end;
end
Lm1: for a be
Real, P be
Subset of (
TOP-REAL n), Q be
Point of (
TOP-REAL n) st P
= { q where q be
Point of (
TOP-REAL n) :
|.(q
- Q).|
<= a } holds P is
convex
proof
let a be
Real, P be
Subset of (
TOP-REAL n), Q be
Point of (
TOP-REAL n);
assume
A1: P
= { q where q be
Point of (
TOP-REAL n) :
|.(q
- Q).|
<= a };
let p1,p2 be
Point of (
TOP-REAL n);
assume p1
in P;
then
A2: ex q1 be
Point of (
TOP-REAL n) st q1
= p1 &
|.(q1
- Q).|
<= a by
A1;
assume
A3: p2
in P;
then
A4: ex q2 be
Point of (
TOP-REAL n) st q2
= p2 &
|.(q2
- Q).|
<= a by
A1;
let x be
object;
assume
A5: x
in (
LSeg (p1,p2));
then
consider r be
Real such that
A6: x
= (((1
- r)
* p1)
+ (r
* p2)) and
A7:
0
<= r and
A8: r
<= 1;
A9: r
=
|.r.| by
A7,
ABSVALUE:def 1;
reconsider q = x as
Point of (
TOP-REAL n) by
A5;
A10:
|.((1
- r)
* (p1
- Q)).|
= (
|.(1
- r).|
*
|.(p1
- Q).|) by
TOPRNS_1: 7;
A11: (1
- r)
>=
0 by
A8,
XREAL_1: 48;
then
A12:
|.(1
- r).|
= (1
- r) by
ABSVALUE:def 1;
per cases ;
suppose
A13: (1
- r)
>
0 ;
0
<=
|.r.| by
COMPLEX1: 46;
then
A14:
|.(r
* (p2
- Q)).|
= (
|.r.|
*
|.(p2
- Q).|) & (
|.r.|
*
|.(p2
- Q).|)
<= (
|.r.|
* a) by
A4,
TOPRNS_1: 7,
XREAL_1: 64;
(((1
- r)
* Q)
+ (r
* Q))
= (((1
* Q)
- (r
* Q))
+ (r
* Q)) by
RLVECT_1: 35
.= (1
* Q) by
RLVECT_4: 1
.= Q by
RLVECT_1:def 8;
then (q
- Q)
= (((((1
- r)
* p1)
+ (r
* p2))
- ((1
- r)
* Q))
- (r
* Q)) by
A6,
RLVECT_1: 27
.= (((((1
- r)
* p1)
- ((1
- r)
* Q))
+ (r
* p2))
- (r
* Q)) by
RLVECT_1:def 3
.= ((((1
- r)
* (p1
- Q))
+ (r
* p2))
- (r
* Q)) by
RLVECT_1: 34
.= (((1
- r)
* (p1
- Q))
+ ((r
* p2)
- (r
* Q))) by
RLVECT_1:def 3
.= (((1
- r)
* (p1
- Q))
+ (r
* (p2
- Q))) by
RLVECT_1: 34;
then
A15:
|.(q
- Q).|
<= (
|.((1
- r)
* (p1
- Q)).|
+
|.(r
* (p2
- Q)).|) by
TOPRNS_1: 29;
(
|.(1
- r).|
*
|.(p1
- Q).|)
<= (
|.(1
- r).|
* a) by
A2,
A12,
A13,
XREAL_1: 64;
then (
|.((1
- r)
* (p1
- Q)).|
+
|.(r
* (p2
- Q)).|)
<= (((1
- r)
* a)
+ (r
* a)) by
A9,
A10,
A12,
A14,
XREAL_1: 7;
then
|.(q
- Q).|
<= a by
A15,
XXREAL_0: 2;
hence thesis by
A1;
end;
suppose (1
- r)
<=
0 ;
then ((1
- r)
+ r)
= (
0
+ r) by
A11;
hence thesis by
A3,
A6,
Th2;
end;
end;
Lm2: for a be
Real, P be
Subset of (
TOP-REAL n), Q be
Point of (
TOP-REAL n) st P
= { q where q be
Point of (
TOP-REAL n) :
|.(q
- Q).|
< a } holds P is
convex
proof
let a be
Real, P be
Subset of (
TOP-REAL n), Q be
Point of (
TOP-REAL n);
assume
A1: P
= { q where q be
Point of (
TOP-REAL n) :
|.(q
- Q).|
< a };
reconsider e = Q as
Point of (
Euclid n) by
TOPREAL3: 8;
let p1,p2 be
Point of (
TOP-REAL n);
assume
A2: p1
in P & p2
in P;
(
Ball (e,a))
= (
Ball (Q,a)) by
Th11
.= P by
A1;
hence thesis by
A2,
TOPREAL3: 21;
end;
registration
let n be
Nat, x be
Point of (
TOP-REAL n);
let r;
cluster (
Ball (x,r)) ->
convex;
coherence by
Lm2;
cluster (
cl_Ball (x,r)) ->
convex;
coherence by
Lm1;
end
definition
let n be
Nat;
let f be
Function of (
TOP-REAL n), (
TOP-REAL n);
::
TOPREAL9:def4
attr f is
homogeneous means
:
Def4: for r be
Real, x be
Point of (
TOP-REAL n) holds (f
. (r
* x))
= (r
* (f
. x));
end
registration
let n;
cluster ((
TOP-REAL n)
--> (
0. (
TOP-REAL n))) ->
homogeneous
additive;
coherence
proof
set f = ((
TOP-REAL n)
--> (
0. (
TOP-REAL n)));
thus f is
homogeneous
proof
let r be
Real, x be
Point of (
TOP-REAL n);
thus (f
. (r
* x))
= (
0. (
TOP-REAL n)) by
FUNCOP_1: 7
.= (r
* (
0. (
TOP-REAL n))) by
RLVECT_1: 10
.= (r
* (f
. x)) by
FUNCOP_1: 7;
end;
let x,y be
Point of (
TOP-REAL n);
thus (f
. (x
+ y))
= (
0. (
TOP-REAL n)) by
FUNCOP_1: 7
.= ((
0. (
TOP-REAL n))
+ (
0. (
TOP-REAL n))) by
RLVECT_1: 4
.= ((f
. x)
+ (
0. (
TOP-REAL n))) by
FUNCOP_1: 7
.= ((f
. x)
+ (f
. y)) by
FUNCOP_1: 7;
end;
end
registration
let n;
cluster
homogeneous
additive
continuous for
Function of (
TOP-REAL n), (
TOP-REAL n);
existence
proof
take ((
TOP-REAL n)
--> (
0. (
TOP-REAL n)));
thus thesis;
end;
end
registration
let a,c be
Real;
cluster (
AffineMap (a,
0 ,c,
0 )) ->
homogeneous
additive;
coherence
proof
set f = (
AffineMap (a,
0 ,c,
0 ));
hereby
let r be
Real, x be
Point of (
TOP-REAL 2);
A1: ((r
* x)
`1 )
= (r
* (x
`1 )) & ((r
* x)
`2 )
= (r
* (x
`2 )) by
TOPREAL3: 4;
thus (f
. (r
* x))
=
|[((a
* ((r
* x)
`1 ))
+
0 ), ((c
* ((r
* x)
`2 ))
+
0 )]| by
JGRAPH_2:def 2
.=
|[(r
* (a
* (x
`1 ))), (r
* (c
* (x
`2 )))]| by
A1
.= (r
*
|[((a
* (x
`1 ))
+
0 ), ((c
* (x
`2 ))
+
0 )]|) by
EUCLID: 58
.= (r
* (f
. x)) by
JGRAPH_2:def 2;
end;
let x,y be
Point of (
TOP-REAL 2);
A2: ((x
+ y)
`1 )
= ((x
`1 )
+ (y
`1 )) & ((x
+ y)
`2 )
= ((x
`2 )
+ (y
`2 )) by
TOPREAL3: 2;
thus (f
. (x
+ y))
=
|[((a
* ((x
+ y)
`1 ))
+
0 ), ((c
* ((x
+ y)
`2 ))
+
0 )]| by
JGRAPH_2:def 2
.=
|[((a
* (x
`1 ))
+ (a
* (y
`1 ))), ((c
* (x
`2 ))
+ (c
* (y
`2 )))]| by
A2
.= (
|[((a
* (x
`1 ))
+
0 ), ((c
* (x
`2 ))
+
0 )]|
+
|[(a
* (y
`1 )), (c
* (y
`2 ))]|) by
EUCLID: 56
.= ((f
. x)
+
|[((a
* (y
`1 ))
+
0 ), ((c
* (y
`2 ))
+
0 )]|) by
JGRAPH_2:def 2
.= ((f
. x)
+ (f
. y)) by
JGRAPH_2:def 2;
end;
end
theorem ::
TOPREAL9:25
for f be
homogeneous
additive
Function of (
TOP-REAL n), (
TOP-REAL n), X be
convex
Subset of (
TOP-REAL n) holds (f
.: X) is
convex
proof
let f be
homogeneous
additive
Function of (
TOP-REAL n), (
TOP-REAL n), X be
convex
Subset of (
TOP-REAL n);
let p,q be
Point of (
TOP-REAL n);
assume p
in (f
.: X);
then
consider p0 be
Point of (
TOP-REAL n) such that
A1: p0
in X and
A2: p
= (f
. p0) by
FUNCT_2: 65;
assume q
in (f
.: X);
then
consider q0 be
Point of (
TOP-REAL n) such that
A3: q0
in X and
A4: q
= (f
. q0) by
FUNCT_2: 65;
A5: (
LSeg (p0,q0))
c= X by
A1,
A3,
JORDAN1:def 1;
let x be
object;
assume x
in (
LSeg (p,q));
then
consider l be
Real such that
A6: x
= (((1
- l)
* p)
+ (l
* q)) and
A7:
0
<= l & l
<= 1;
set a = (((1
- l)
* p0)
+ (l
* q0));
A8: a
in (
LSeg (p0,q0)) by
A7;
(f
. a)
= ((f
. ((1
- l)
* p0))
+ (f
. (l
* q0))) by
VECTSP_1:def 20
.= ((f
. ((1
- l)
* p0))
+ (l
* (f
. q0))) by
Def4
.= x by
A2,
A4,
A6,
Def4;
hence thesis by
A8,
A5,
FUNCT_2: 35;
end;
reserve V for
RealLinearSpace,
p,q,x for
Element of V;
definition
let V, p, q;
::
TOPREAL9:def5
func
halfline (p,q) ->
Subset of V equals { (((1
- l)
* p)
+ (l
* q)) where l be
Real :
0
<= l };
coherence
proof
set X = { (((1
- l)
* p)
+ (l
* q)) where l be
Real :
0
<= l };
X
c= the
carrier of V
proof
let x be
object;
assume x
in X;
then ex l be
Real st x
= (((1
- l)
* p)
+ (l
* q)) &
0
<= l;
hence thesis;
end;
hence thesis;
end;
end
theorem ::
TOPREAL9:26
for x be
set holds x
in (
halfline (p,q)) iff ex l be
Real st x
= (((1
- l)
* p)
+ (l
* q)) &
0
<= l;
registration
let V, p, q;
cluster (
halfline (p,q)) -> non
empty;
coherence
proof
(((1
-
0 )
* p)
+ (
0
* q))
in (
halfline (p,q));
hence thesis;
end;
end
theorem ::
TOPREAL9:27
Th25: p
in (
halfline (p,q))
proof
(((1
-
0 )
* p)
+ (
0
* q))
= (p
+ (
0
* q)) by
RLVECT_1:def 8
.= (p
+ (
0. V)) by
RLVECT_1: 10
.= p by
RLVECT_1: 4;
hence thesis;
end;
theorem ::
TOPREAL9:28
Th26: q
in (
halfline (p,q))
proof
(((1
- 1)
* p)
+ (1
* q))
= ((
0
* p)
+ q) by
RLVECT_1:def 8
.= ((
0. V)
+ q) by
RLVECT_1: 10
.= q by
RLVECT_1: 4;
hence thesis;
end;
theorem ::
TOPREAL9:29
Th27: (
halfline (p,p))
=
{p}
proof
hereby
let d be
object;
assume d
in (
halfline (p,p));
then ex r be
Real st d
= (((1
- r)
* p)
+ (r
* p)) &
0
<= r;
then d
= p by
Th2;
hence d
in
{p} by
TARSKI:def 1;
end;
let d be
object;
assume d
in
{p};
then d
= p by
TARSKI:def 1;
hence thesis by
Th25;
end;
theorem ::
TOPREAL9:30
Th28: x
in (
halfline (p,q)) implies (
halfline (p,x))
c= (
halfline (p,q))
proof
assume x
in (
halfline (p,q));
then
consider R be
Real such that
A1: x
= (((1
- R)
* p)
+ (R
* q)) and
A2:
0
<= R;
let d be
object;
assume
A3: d
in (
halfline (p,x));
then
reconsider d as
Point of V;
consider r be
Real such that
A4: d
= (((1
- r)
* p)
+ (r
* x)) and
A5:
0
<= r by
A3;
set o = (r
* R);
d
= (((1
- r)
* p)
+ ((r
* ((1
- R)
* p))
+ (r
* (R
* q)))) by
A1,
A4,
RLVECT_1:def 5
.= ((((1
- r)
* p)
+ (r
* ((1
- R)
* p)))
+ (r
* (R
* q))) by
RLVECT_1:def 3
.= ((((1
- r)
* p)
+ ((r
* (1
- R))
* p))
+ (r
* (R
* q))) by
RLVECT_1:def 7
.= ((((1
- r)
+ (r
* (1
- R)))
* p)
+ (r
* (R
* q))) by
RLVECT_1:def 6
.= (((1
- o)
* p)
+ (o
* q)) by
RLVECT_1:def 7;
hence thesis by
A2,
A5;
end;
theorem ::
TOPREAL9:31
x
in (
halfline (p,q)) & x
<> p implies (
halfline (p,q))
= (
halfline (p,x))
proof
assume
A1: x
in (
halfline (p,q));
then
consider R be
Real such that
A2: x
= (((1
- R)
* p)
+ (R
* q)) and
A3:
0
<= R;
assume
A4: x
<> p;
thus (
halfline (p,q))
c= (
halfline (p,x))
proof
let d be
object;
assume
A5: d
in (
halfline (p,q));
then
reconsider d as
Point of V;
consider r be
Real such that
A6: d
= (((1
- r)
* p)
+ (r
* q)) and
A7:
0
<= r by
A5;
set o = (r
/ R);
R
<>
0 by
A2,
A4,
Th2;
then (o
* R)
= r by
XCMPLX_1: 87;
then d
= ((((1
- o)
+ (o
* (1
- R)))
* p)
+ (o
* (R
* q))) by
A6,
RLVECT_1:def 7
.= ((((1
- o)
* p)
+ ((o
* (1
- R))
* p))
+ (o
* (R
* q))) by
RLVECT_1:def 6
.= ((((1
- o)
* p)
+ (o
* ((1
- R)
* p)))
+ (o
* (R
* q))) by
RLVECT_1:def 7
.= (((1
- o)
* p)
+ ((o
* ((1
- R)
* p))
+ (o
* (R
* q)))) by
RLVECT_1:def 3
.= (((1
- o)
* p)
+ (o
* (((1
- R)
* p)
+ (R
* q)))) by
RLVECT_1:def 5;
hence thesis by
A2,
A3,
A7;
end;
thus thesis by
A1,
Th28;
end;
theorem ::
TOPREAL9:32
(
LSeg (p,q))
c= (
halfline (p,q))
proof
let a be
object;
assume a
in (
LSeg (p,q));
then ex r be
Real st
0
<= r & r
<= 1 & a
= (((1
- r)
* p)
+ (r
* q)) by
RLTOPSP1: 76;
hence thesis;
end;
registration
let V, p, q;
cluster (
halfline (p,q)) ->
convex;
coherence
proof
let u,v be
Point of V;
set P = (
halfline (p,q));
assume u
in P;
then
consider a be
Real such that
A1: u
= (((1
- a)
* p)
+ (a
* q)) and
A2:
0
<= a;
assume v
in P;
then
consider b be
Real such that
A3: v
= (((1
- b)
* p)
+ (b
* q)) and
A4:
0
<= b;
let x be
object;
assume x
in (
LSeg (u,v));
then
consider r be
Real such that
A5:
0
<= r and
A6: r
<= 1 and
A7: x
= (((1
- r)
* u)
+ (r
* v)) by
RLTOPSP1: 76;
set o = (((1
- r)
* a)
+ (r
* b));
A8: (1
- r)
>= (r
- r) by
A6,
XREAL_1: 13;
x
= ((((1
- r)
* ((1
- a)
* p))
+ ((1
- r)
* (a
* q)))
+ (r
* (((1
- b)
* p)
+ (b
* q)))) by
A1,
A3,
A7,
RLVECT_1:def 5
.= ((((1
- r)
* ((1
- a)
* p))
+ ((1
- r)
* (a
* q)))
+ ((r
* ((1
- b)
* p))
+ (r
* (b
* q)))) by
RLVECT_1:def 5
.= ((((1
- r)
* ((1
- a)
* p))
+ ((r
* ((1
- b)
* p))
+ (r
* (b
* q))))
+ ((1
- r)
* (a
* q))) by
RLVECT_1:def 3
.= (((((1
- r)
* ((1
- a)
* p))
+ (r
* ((1
- b)
* p)))
+ (r
* (b
* q)))
+ ((1
- r)
* (a
* q))) by
RLVECT_1:def 3
.= ((((((1
- r)
* (1
- a))
* p)
+ (r
* ((1
- b)
* p)))
+ (r
* (b
* q)))
+ ((1
- r)
* (a
* q))) by
RLVECT_1:def 7
.= ((((((1
- r)
* (1
- a))
* p)
+ ((r
* (1
- b))
* p))
+ (r
* (b
* q)))
+ ((1
- r)
* (a
* q))) by
RLVECT_1:def 7
.= ((((((1
- r)
* (1
- a))
* p)
+ ((r
* (1
- b))
* p))
+ ((r
* b)
* q))
+ ((1
- r)
* (a
* q))) by
RLVECT_1:def 7
.= ((((((1
- r)
* (1
- a))
* p)
+ ((r
* (1
- b))
* p))
+ ((r
* b)
* q))
+ (((1
- r)
* a)
* q)) by
RLVECT_1:def 7
.= ((((((1
- r)
* (1
- a))
+ (r
* (1
- b)))
* p)
+ ((r
* b)
* q))
+ (((1
- r)
* a)
* q)) by
RLVECT_1:def 6
.= (((((1
- r)
* (1
- a))
+ (r
* (1
- b)))
* p)
+ (((r
* b)
* q)
+ (((1
- r)
* a)
* q))) by
RLVECT_1:def 3
.= (((1
- o)
* p)
+ (o
* q)) by
RLVECT_1:def 6;
hence thesis by
A2,
A4,
A5,
A8;
end;
end
reserve p,q,x for
Point of (
TOP-REAL n);
theorem ::
TOPREAL9:33
Th31: y
in (
Sphere (x,r)) & z
in (
Ball (x,r)) implies ((
LSeg (y,z))
/\ (
Sphere (x,r)))
=
{y}
proof
set s = y, t = z;
assume that
A1: s
in (
Sphere (x,r)) and
A2: t
in (
Ball (x,r));
hereby
let m be
object;
assume
A3: m
in ((
LSeg (s,t))
/\ (
Sphere (x,r)));
then
reconsider w = m as
Point of (
TOP-REAL n);
w
in (
LSeg (s,t)) by
A3,
XBOOLE_0:def 4;
then
consider d be
Real such that
A4:
0
<= d and
A5: d
<= 1 and
A6: w
= (((1
- d)
* s)
+ (d
* t)) by
RLTOPSP1: 76;
A7:
|.(d
* (t
- x)).|
= (
|.d.|
*
|.(t
- x).|) by
TOPRNS_1: 7
.= (d
*
|.(t
- x).|) by
A4,
ABSVALUE:def 1;
(d
- 1)
<= (1
- 1) by
A5,
XREAL_1: 9;
then
A8: (
-
0 qua
Element of
NAT )
<= (
- (d
- 1));
A9:
|.((1
- d)
* (s
- x)).|
= (
|.(1
- d).|
*
|.(s
- x).|) by
TOPRNS_1: 7
.= ((1
- d)
*
|.(s
- x).|) by
A8,
ABSVALUE:def 1
.= ((1
- d)
* r) by
A1,
Th7;
m
in (
Sphere (x,r)) by
A3,
XBOOLE_0:def 4;
then
A10: r
=
|.(w
- x).| by
Th7
.=
|.((((1
- d)
* s)
+ (d
* t))
- (((1
- d)
+ d)
* x)).| by
A6,
RLVECT_1:def 8
.=
|.((((1
- d)
* s)
+ (d
* t))
- (((1
- d)
* x)
+ (d
* x))).| by
RLVECT_1:def 6
.=
|.(((((1
- d)
* s)
+ (d
* t))
- ((1
- d)
* x))
- (d
* x)).| by
RLVECT_1: 27
.=
|.(((((1
- d)
* s)
- ((1
- d)
* x))
+ (d
* t))
- (d
* x)).| by
RLVECT_1:def 3
.=
|.((((1
- d)
* (s
- x))
+ (d
* t))
- (d
* x)).| by
RLVECT_1: 34
.=
|.(((1
- d)
* (s
- x))
+ ((d
* t)
- (d
* x))).| by
RLVECT_1:def 3
.=
|.(((1
- d)
* (s
- x))
+ (d
* (t
- x))).| by
RLVECT_1: 34;
per cases by
A4;
suppose
A11: d
>
0 ;
|.(t
- x).|
< r by
A2,
Th5;
then (d
*
|.(t
- x).|)
< (d
* r) by
A11,
XREAL_1: 68;
then (((1
- d)
* r)
+ (d
*
|.(t
- x).|))
< (((1
- d)
* r)
+ (d
* r)) by
XREAL_1: 8;
hence m
in
{s} by
A10,
A9,
A7,
TOPRNS_1: 29;
end;
suppose d
=
0 ;
then m
= ((1
* s)
+ (
0. (
TOP-REAL n))) by
A6,
RLVECT_1: 10
.= (1
* s) by
RLVECT_1: 4
.= s by
RLVECT_1:def 8;
hence m
in
{s} by
TARSKI:def 1;
end;
end;
let m be
object;
A12: s
in (
LSeg (s,t)) by
RLTOPSP1: 68;
assume m
in
{s};
then m
= s by
TARSKI:def 1;
hence thesis by
A1,
A12,
XBOOLE_0:def 4;
end;
theorem ::
TOPREAL9:34
Th32: y
in (
Sphere (x,r)) & z
in (
Sphere (x,r)) implies ((
LSeg (y,z))
\
{y, z})
c= (
Ball (x,r))
proof
assume that
A1: y
in (
Sphere (x,r)) and
A2: z
in (
Sphere (x,r));
per cases ;
suppose y
= z;
then (
LSeg (y,z))
=
{y} &
{y, z}
=
{y} by
ENUMSET1: 29,
RLTOPSP1: 70;
then ((
LSeg (y,z))
\
{y, z})
=
{} by
XBOOLE_1: 37;
hence thesis;
end;
suppose
A3: y
<> z;
the
carrier of (
TOP-REAL n)
= (
REAL n) by
EUCLID: 22
.= (n
-tuples_on
REAL );
then
reconsider xf = x, yf = y, zf = z as
Element of (n
-tuples_on
REAL );
reconsider yyf = yf, zzf = zf, xxf = xf as
Element of (
REAL n);
reconsider y1 = (y
- x), z1 = (z
- x) as
FinSequence of
REAL ;
set X =
|((y
- x), (z
- x))|;
let a be
object;
A4: (
Sum (
sqr (zf
- xf)))
= (
|.z1.|
^2 ) by
Th3;
A5: (
|.(z
- x).|
^2 )
= (r
^2 ) by
A2,
Th7;
assume
A6: a
in ((
LSeg (y,z))
\
{y, z});
then
reconsider R = a as
Point of (
TOP-REAL n);
A7: R
in (
LSeg (y,z)) by
A6,
XBOOLE_0:def 5;
then
consider l be
Real such that
A8:
0
<= l and
A9: l
<= 1 and
A10: R
= (((1
- l)
* y)
+ (l
* z)) by
RLTOPSP1: 76;
set l1 = (1
- l);
reconsider W1 = (l1
* (y
- x)), W2 = (l
* (z
- x)) as
Element of (
REAL n) by
EUCLID: 22;
A11: (
Sum (
sqr (yf
- zf)))
>=
0 by
RVSUM_1: 86;
reconsider Rf = (R
- x) as
FinSequence of
REAL ;
A12: (W1
+ W2)
= (((l1
* y)
- (l1
* x))
+ (l
* (z
- x))) by
RLVECT_1: 34
.= (((l1
* y)
- (l1
* x))
+ ((l
* z)
- (l
* x))) by
RLVECT_1: 34
.= ((((l1
* y)
- (l1
* x))
+ (l
* z))
- (l
* x)) by
RLVECT_1:def 3
.= ((((l1
* y)
+ (l
* z))
- (l1
* x))
- (l
* x)) by
RLVECT_1:def 3
.= (((l1
* y)
+ (l
* z))
- ((l1
* x)
+ (l
* x))) by
RLVECT_1: 27
.= (((l1
* y)
+ (l
* z))
- (((1
* x)
- (l
* x))
+ (l
* x))) by
RLVECT_1: 35
.= (((l1
* y)
+ (l
* z))
- (1
* x)) by
RLVECT_4: 1
.= Rf by
A10,
RLVECT_1:def 8;
reconsider W1, W2 as
Element of (n
-tuples_on
REAL );
A13: (
mlt (W1,W2))
= (l1
* (
mlt ((yf
- xf),(l
* (zf
- xf))))) by
RVSUM_1: 65;
A14: (
sqr W1)
= ((l1
^2 )
* (
sqr (yf
- xf))) by
RVSUM_1: 58;
(
Sum (
sqr Rf))
>=
0 by
RVSUM_1: 86;
then (
|.(R
- x).|
^2 )
= (
Sum (
sqr Rf)) by
SQUARE_1:def 2
.= (
Sum (((
sqr W1)
+ (2
* (
mlt (W1,W2))))
+ (
sqr W2))) by
A12,
RVSUM_1: 68
.= ((
Sum ((
sqr W1)
+ (2
* (
mlt (W1,W2)))))
+ (
Sum (
sqr W2))) by
RVSUM_1: 89
.= (((
Sum (
sqr W1))
+ (
Sum (2
* (
mlt (W1,W2)))))
+ (
Sum (
sqr W2))) by
RVSUM_1: 89
.= ((((l1
^2 )
* (
Sum (
sqr (yf
- xf))))
+ (
Sum (2
* (
mlt (W1,W2)))))
+ (
Sum (
sqr (l
* (zf
- xf))))) by
A14,
RVSUM_1: 87
.= ((((l1
^2 )
* (
Sum (
sqr (yf
- xf))))
+ (
Sum (2
* (
mlt (W1,W2)))))
+ (
Sum ((l
^2 )
* (
sqr (zf
- xf))))) by
RVSUM_1: 58
.= ((((l1
^2 )
* (
Sum (
sqr (yf
- xf))))
+ (
Sum (2
* (
mlt (W1,W2)))))
+ ((l
^2 )
* (
Sum (
sqr (zf
- xf))))) by
RVSUM_1: 87
.= ((((l1
^2 )
* (
|.y1.|
^2 ))
+ (
Sum (2
* (
mlt (W1,W2)))))
+ ((l
^2 )
* (
Sum (
sqr (zf
- xf))))) by
Th3
.= ((((l1
^2 )
* (r
^2 ))
+ (
Sum (2
* (
mlt (W1,W2)))))
+ ((l
^2 )
* (
|.z1.|
^2 ))) by
A1,
A4,
Th7
.= ((((l1
^2 )
* (r
^2 ))
+ (2
* (
Sum (
mlt (W1,W2)))))
+ ((l
^2 )
* (r
^2 ))) by
A5,
RVSUM_1: 87
.= ((((l1
^2 )
* (r
^2 ))
+ (2
* (
Sum (l1
* (l
* (
mlt ((yf
- xf),(zf
- xf))))))))
+ ((l
^2 )
* (r
^2 ))) by
A13,
RVSUM_1: 65
.= ((((l1
^2 )
* (r
^2 ))
+ (2
* (
Sum ((l1
* l)
* (
mlt ((yf
- xf),(zf
- xf)))))))
+ ((l
^2 )
* (r
^2 ))) by
RVSUM_1: 49
.= ((((l1
^2 )
* (r
^2 ))
+ (2
* ((l1
* l)
* (
Sum (
mlt ((yf
- xf),(zf
- xf)))))))
+ ((l
^2 )
* (r
^2 ))) by
RVSUM_1: 87
.= ((((l1
^2 )
* (r
^2 ))
+ (((2
* l1)
* l)
* (
Sum (
mlt ((yf
- xf),(zf
- xf))))))
+ ((l
^2 )
* (r
^2 )))
.= ((((l1
^2 )
* (r
^2 ))
+ (((2
* l1)
* l)
* X))
+ ((l
^2 )
* (r
^2 ))) by
RVSUM_1:def 16
.= (((((1
- (2
* l))
+ (l
^2 ))
+ (l
^2 ))
* (r
^2 ))
+ (((2
* l)
* l1)
* X));
then
A15: ((
|.(R
- x).|
^2 )
- (r
^2 ))
= (((2
* l)
* l1)
* ((
- (r
^2 ))
+ X));
now
assume l
=
0 ;
then R
= y by
A10,
Th2;
then R
in
{y, z} by
TARSKI:def 2;
hence contradiction by
A6,
XBOOLE_0:def 5;
end;
then
A16: (2
* l)
>
0 by
A8,
XREAL_1: 129;
A17:
now
assume l1
=
0 ;
then R
= z by
A10,
Th2;
then R
in
{y, z} by
TARSKI:def 2;
hence contradiction by
A6,
XBOOLE_0:def 5;
end;
(1
- 1)
<= l1 by
A9,
XREAL_1: 13;
then
A18: ((2
* l)
* l1)
>
0 by
A16,
A17,
XREAL_1: 129;
A19: (
|.(y
- x).|
^2 )
= (r
^2 ) by
A1,
Th7;
A20:
now
assume
|.(R
- x).|
= r;
then (X
- (r
^2 ))
=
0 by
A15,
A18,
XCMPLX_1: 6;
then
0
= (((
|.(y
- x).|
^2 )
- (2
* X))
+ (
|.(z
- x).|
^2 )) by
A2,
A19,
Th7
.= (
|.((y
- x)
- (z
- x)).|
^2 ) by
EUCLID_2: 46
.= (
|.(((y
- x)
- z)
+ x).|
^2 ) by
RLVECT_1: 29
.= (
|.(((y
- x)
+ x)
- z).|
^2 ) by
RLVECT_1:def 3
.= (
|.(yf
- zf).|
^2 ) by
RLVECT_4: 1
.= (
Sum (
sqr (yf
- zf))) by
A11,
SQUARE_1:def 2;
then (yf
- zf)
= (n
|->
0 ) by
RVSUM_1: 91;
hence contradiction by
A3,
RVSUM_1: 38;
end;
(
Sphere (x,r))
c= (
cl_Ball (x,r)) by
Th15;
then (
LSeg (y,z))
c= (
cl_Ball (x,r)) by
A1,
A2,
JORDAN1:def 1;
then
|.(R
- x).|
<= r by
A7,
Th6;
then
|.(R
- x).|
< r by
A20,
XXREAL_0: 1;
hence thesis;
end;
end;
theorem ::
TOPREAL9:35
Th33: y
in (
Sphere (x,r)) & z
in (
Sphere (x,r)) implies ((
LSeg (y,z))
/\ (
Sphere (x,r)))
=
{y, z}
proof
A1: y
in (
LSeg (y,z)) & z
in (
LSeg (y,z)) by
RLTOPSP1: 68;
assume
A2: y
in (
Sphere (x,r)) & z
in (
Sphere (x,r));
then
A3: ((
LSeg (y,z))
\
{y, z})
c= (
Ball (x,r)) by
Th32;
hereby
let a be
object;
assume
A4: a
in ((
LSeg (y,z))
/\ (
Sphere (x,r)));
assume
A5: not a
in
{y, z};
a
in (
LSeg (y,z)) by
A4,
XBOOLE_0:def 4;
then
A6: a
in ((
LSeg (y,z))
\
{y, z}) by
A5,
XBOOLE_0:def 5;
A7: (
Ball (x,r))
misses (
Sphere (x,r)) by
Th17;
a
in (
Sphere (x,r)) by
A4,
XBOOLE_0:def 4;
hence contradiction by
A3,
A6,
A7,
XBOOLE_0: 3;
end;
let a be
object;
assume a
in
{y, z};
then a
= y or a
= z by
TARSKI:def 2;
hence thesis by
A2,
A1,
XBOOLE_0:def 4;
end;
theorem ::
TOPREAL9:36
Th34: y
in (
Sphere (x,r)) & z
in (
Sphere (x,r)) implies ((
halfline (y,z))
/\ (
Sphere (x,r)))
=
{y, z}
proof
assume that
A1: y
in (
Sphere (x,r)) and
A2: z
in (
Sphere (x,r));
per cases ;
suppose
A3: y
= z;
then
A4:
{y, z}
=
{y} by
ENUMSET1: 29;
A5: (
halfline (y,z))
=
{y} by
A3,
Th27;
hence for m be
object st m
in ((
halfline (y,z))
/\ (
Sphere (x,r))) holds m
in
{y, z} by
A4,
XBOOLE_0:def 4;
let m be
object;
assume
A6: m
in
{y, z};
then m
= y by
A4,
TARSKI:def 1;
hence thesis by
A1,
A5,
A4,
A6,
XBOOLE_0:def 4;
end;
suppose
A7: y
<> z;
hereby
let m be
object;
assume
A8: m
in ((
halfline (y,z))
/\ (
Sphere (x,r)));
then
A9: m
in (
Sphere (x,r)) by
XBOOLE_0:def 4;
reconsider w = m as
Point of (
TOP-REAL n) by
A8;
m
in (
halfline (y,z)) by
A8,
XBOOLE_0:def 4;
then
consider R be
Real such that
A10: m
= (((1
- R)
* y)
+ (R
* z)) and
A11:
0
<= R;
reconsider R as
Real;
per cases by
A11,
XXREAL_0: 1;
suppose R
=
0 ;
then m
= y by
A10,
Th2;
hence m
in
{y, z} by
TARSKI:def 2;
end;
suppose R
= 1;
then m
= z by
A10,
Th2;
hence m
in
{y, z} by
TARSKI:def 2;
end;
suppose
A12: R
>
0 & R
< 1;
A13:
now
assume m
in
{y, z};
then m
= y or m
= z by
TARSKI:def 2;
hence contradiction by
A7,
A10,
A12,
Th2;
end;
w
in (
LSeg (y,z)) by
A10,
A12;
then
A14: m
in ((
LSeg (y,z))
\
{y, z}) by
A13,
XBOOLE_0:def 5;
((
LSeg (y,z))
\
{y, z})
c= (
Ball (x,r)) by
A1,
A2,
Th32;
then
|.(w
- x).|
< r by
A14,
Th5;
hence m
in
{y, z} by
A9,
Th7;
end;
suppose
A15: R
> 1;
then
A16: (1
/ R)
< 1 by
XREAL_1: 212;
A17: (((1
- (1
/ R))
* y)
+ ((1
/ R)
* w))
= (((1
- (1
/ R))
* y)
+ (((1
/ R)
* ((1
- R)
* y))
+ ((1
/ R)
* (R
* z)))) by
A10,
RLVECT_1:def 5
.= (((1
- (1
/ R))
* y)
+ (((1
/ R)
* ((1
- R)
* y))
+ (((1
/ R)
* R)
* z))) by
RLVECT_1:def 7
.= (((1
- (1
/ R))
* y)
+ (((1
/ R)
* ((1
- R)
* y))
+ (1
* z))) by
A15,
XCMPLX_1: 87
.= (((1
- (1
/ R))
* y)
+ (((1
/ R)
* ((1
- R)
* y))
+ z)) by
RLVECT_1:def 8
.= ((((1
- (1
/ R))
* y)
+ ((1
/ R)
* ((1
- R)
* y)))
+ z) by
RLVECT_1:def 3
.= ((((1
- (1
/ R))
* y)
+ (((1
/ R)
* (1
- R))
* y))
+ z) by
RLVECT_1:def 7
.= ((((1
- (1
/ R))
+ ((1
/ R)
* (1
- R)))
* y)
+ z) by
RLVECT_1:def 6
.= (((((1
- (1
/ R))
+ ((1
/ R)
* 1))
- ((1
/ R)
* R))
* y)
+ z)
.= (((((1
- (1
/ R))
+ ((1
/ R)
* 1))
- 1)
* y)
+ z) by
A15,
XCMPLX_1: 87
.= ((
0. (
TOP-REAL n))
+ z) by
RLVECT_1: 10
.= z by
RLVECT_1: 4;
A18:
now
assume z
in
{y, w};
then z
= y or z
= w by
TARSKI:def 2;
hence contradiction by
A7,
A16,
A17,
Th2;
end;
z
in (
LSeg (y,w)) by
A15,
A16,
A17;
then
A19: z
in ((
LSeg (y,w))
\
{y, w}) by
A18,
XBOOLE_0:def 5;
((
LSeg (y,w))
\
{y, w})
c= (
Ball (x,r)) by
A1,
A9,
Th32;
then
|.(z
- x).|
< r by
A19,
Th5;
hence m
in
{y, z} by
A2,
Th7;
end;
end;
let m be
object;
assume m
in
{y, z};
then
A20: m
= y or m
= z by
TARSKI:def 2;
y
in (
halfline (y,z)) & z
in (
halfline (y,z)) by
Th25,
Th26;
hence thesis by
A1,
A2,
A20,
XBOOLE_0:def 4;
end;
end;
theorem ::
TOPREAL9:37
Th35: for S,T,X be
Element of (
REAL n) st S
= y & T
= z & X
= x holds 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))))) implies ex e be
Point of (
TOP-REAL n) st
{e}
= ((
halfline (y,z))
/\ (
Sphere (x,r))) & e
= (((1
- a)
* y)
+ (a
* z))
proof
let S,T,X be
Element of (
REAL n) such that
A1: S
= y and
A2: T
= z and
A3: X
= x;
set s = y, t = z;
A4: (
Sum (
sqr (T
- S)))
>=
0 by
RVSUM_1: 86;
then
A5: (
|.(T
- S).|
^2 )
= (
Sum (
sqr (T
- S))) by
SQUARE_1:def 2;
set A = (
Sum (
sqr (T
- S)));
assume that
A6: s
<> t and
A7: s
in (
Ball (x,r)) and
A8: 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)))));
A9:
|.(T
- S).|
<>
0 by
A1,
A2,
A6,
EUCLID: 16;
A10:
now
assume A
<=
0 ;
then A
=
0 by
RVSUM_1: 86;
hence contradiction by
A9,
SQUARE_1: 17;
end;
set C = ((
Sum (
sqr (S
- X)))
- (r
^2 ));
set B = (2
*
|((t
- s), (s
- x))|);
A11: r
=
0 or r
<>
0 ;
(
Sum (
sqr (S
- X)))
>=
0 by
RVSUM_1: 86;
then
A12: (
|.(S
- X).|
^2 )
= (
Sum (
sqr (S
- X))) by
SQUARE_1:def 2;
|.(s
- x).|
< r by
A7,
Th5;
then ((
sqrt (
Sum (
sqr (S
- X))))
^2 )
< (r
^2 ) by
A1,
A3,
SQUARE_1: 16;
then
A13: C
<
0 by
A12,
XREAL_1: 49;
then
A14: (C
/ A)
<
0 by
A10,
XREAL_1: 141;
set l2 = (((
- B)
+ (
sqrt (
delta (A,B,C))))
/ (2
* A));
set l1 = (((
- B)
- (
sqrt (
delta (A,B,C))))
/ (2
* A));
take e1 = (((1
- l2)
* s)
+ (l2
* t));
A15:
0
<= (
- (
- r)) by
A7;
A16: (
delta (A,B,C))
= ((B
^2 )
- ((4
* A)
* C)) & (B
^2 )
>=
0 by
QUIN_1:def 1,
XREAL_1: 63;
A17: for x be
Real holds (
Polynom (A,B,C,x))
= (
Quard (A,l1,l2,x))
proof
let x be
Real;
thus (
Polynom (A,B,C,x))
= (((A
* (x
^2 ))
+ (B
* x))
+ C) by
POLYEQ_1:def 2
.= ((A
* (x
- l1))
* (x
- l2)) by
A10,
A13,
A16,
QUIN_1: 16
.= (A
* ((x
- l1)
* (x
- l2)))
.= (
Quard (A,l1,l2,x)) by
POLYEQ_1:def 3;
end;
then (C
/ A)
= (l1
* l2) by
A10,
POLYEQ_1: 11;
then
A18: l1
<
0 & l2
>
0 or l1
>
0 & l2
<
0 by
A14,
XREAL_1: 133;
A19: (((A
* (l2
^2 ))
+ (B
* l2))
- (
- C))
= (
Polynom (A,B,C,l2)) by
POLYEQ_1:def 2
.= (
Quard (A,l1,l2,l2)) by
A17
.= (A
* ((l2
- l1)
* (l2
- l2))) by
POLYEQ_1:def 3
.=
0 ;
(
|.(e1
- x).|
^2 )
= (
|.((((1
* s)
- (l2
* s))
+ (l2
* t))
- x).|
^2 ) by
RLVECT_1: 35
.= (
|.(((s
- (l2
* s))
+ (l2
* t))
- x).|
^2 ) by
RLVECT_1:def 8
.= (
|.(((s
+ (l2
* t))
- (l2
* s))
- x).|
^2 ) by
RLVECT_1:def 3
.= (
|.((s
+ ((l2
* t)
- (l2
* s)))
- x).|
^2 ) by
RLVECT_1:def 3
.= (
|.((s
- x)
+ ((l2
* t)
- (l2
* s))).|
^2 ) by
RLVECT_1:def 3
.= (
|.((s
- x)
+ (l2
* (t
- s))).|
^2 ) by
RLVECT_1: 34
.= (((
|.(s
- x).|
^2 )
+ (2
*
|((l2
* (t
- s)), (s
- x))|))
+ (
|.(l2
* (t
- s)).|
^2 )) by
EUCLID_2: 45
.= (((
Sum (
sqr (S
- X)))
+ (2
* (l2
*
|((t
- s), (s
- x))|)))
+ (
|.(l2
* (t
- s)).|
^2 )) by
A12,
A1,
A3,
EUCLID_2: 19
.= (((
Sum (
sqr (S
- X)))
+ ((2
* l2)
*
|((t
- s), (s
- x))|))
+ ((
|.l2.|
*
|.(t
- s).|)
^2 )) by
TOPRNS_1: 7
.= (((
Sum (
sqr (S
- X)))
+ ((2
* l2)
*
|((t
- s), (s
- x))|))
+ ((
|.l2.|
^2 )
* (
|.(t
- s).|
^2 )))
.= (((
Sum (
sqr (S
- X)))
+ (l2
* (2
*
|((t
- s), (s
- x))|)))
+ ((l2
^2 )
* (
|.(T
- S).|
^2 ))) by
A1,
A2,
COMPLEX1: 75
.= (((
Sum (
sqr (S
- X)))
+ (l2
* B))
+ ((l2
^2 )
* A)) by
A4,
SQUARE_1:def 2
.= (r
^2 ) by
A19;
then
|.(e1
- x).|
= r or
|.(e1
- x).|
= (
- r) by
SQUARE_1: 40;
then
A20: e1
in (
Sphere (x,r)) by
A15,
A11;
A21: ((4
* A)
* C)
<
0 by
A10,
A13,
XREAL_1: 129,
XREAL_1: 132;
then
A22: e1
in (
halfline (s,t)) by
A10,
A16,
A18,
QUIN_1: 25;
hereby
let d be
object;
assume d
in
{e1};
then d
= e1 by
TARSKI:def 1;
hence d
in ((
halfline (s,t))
/\ (
Sphere (x,r))) by
A22,
A20,
XBOOLE_0:def 4;
end;
hereby
let d be
object;
assume
A23: d
in ((
halfline (s,t))
/\ (
Sphere (x,r)));
then d
in (
halfline (s,t)) by
XBOOLE_0:def 4;
then
consider l be
Real such that
A24: d
= (((1
- l)
* s)
+ (l
* t)) and
A25:
0
<= l;
A26: (
|.(l
* (t
- s)).|
^2 )
= ((
|.l.|
*
|.(t
- s).|)
^2 ) by
TOPRNS_1: 7
.= ((
|.l.|
^2 )
* (
|.(t
- s).|
^2 ))
.= ((l
^2 )
* (
|.(t
- s).|
^2 )) by
COMPLEX1: 75;
d
in (
Sphere (x,r)) by
A23,
XBOOLE_0:def 4;
then r
=
|.((((1
- l)
* s)
+ (l
* t))
- x).| by
A24,
Th7
.=
|.((((1
* s)
- (l
* s))
+ (l
* t))
- x).| by
RLVECT_1: 35
.=
|.(((s
- (l
* s))
+ (l
* t))
- x).| by
RLVECT_1:def 8
.=
|.((s
- ((l
* s)
- (l
* t)))
- x).| by
RLVECT_1: 29
.=
|.((s
+ (
- ((l
* s)
- (l
* t))))
+ (
- x)).|
.=
|.((s
+ (
- x))
+ (
- ((l
* s)
- (l
* t)))).| by
RLVECT_1:def 3
.=
|.((s
- x)
- ((l
* s)
- (l
* t))).|
.=
|.((s
+ (
- x))
+ (
- ((l
* s)
- (l
* t)))).|
.=
|.((s
- x)
+ (
- (l
* (s
- t)))).| by
RLVECT_1: 34
.=
|.((s
- x)
+ (l
* (
- (s
- t)))).| by
RLVECT_1: 25
.=
|.((s
- x)
+ (l
* (t
- s))).| by
RLVECT_1: 33;
then (r
^2 )
= (((
|.(s
- x).|
^2 )
+ (2
*
|((l
* (t
- s)), (s
- x))|))
+ (
|.(l
* (t
- s)).|
^2 )) by
EUCLID_2: 45
.= (((
|.(s
- x).|
^2 )
+ (2
* (l
*
|((t
- s), (s
- x))|)))
+ (
|.(l
* (t
- s)).|
^2 )) by
EUCLID_2: 19;
then (((A
* (l
^2 ))
+ (B
* l))
+ C)
=
0 by
A5,
A12,
A1,
A3,
A2,
A26;
then (
Polynom (A,B,C,l))
=
0 by
POLYEQ_1:def 2;
then l
= l1 or l
= l2 by
A10,
A13,
A16,
POLYEQ_1: 5;
hence d
in
{e1} by
A10,
A21,
A16,
A18,
A24,
A25,
QUIN_1: 25,
TARSKI:def 1;
end;
thus thesis by
A8;
end;
theorem ::
TOPREAL9:38
Th36: for S,T,Y be
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 be
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
let S,T,Y be
Element of (
REAL n) such that
A1: S
= (((1
/ 2)
* y)
+ ((1
/ 2)
* z)) & T
= z & Y
= x;
reconsider G = x as
Point of (
Euclid n) by
TOPREAL3: 8;
set s = y, t = z;
set X = (((1
/ 2)
* s)
+ ((1
/ 2)
* t));
assume that
A2: s
<> t and
A3: s
in (
Sphere (x,r)) and
A4: t
in (
cl_Ball (x,r));
A5: (
Ball (G,r))
= (
Ball (x,r)) by
Th11;
A6: (
Sphere (x,r))
c= (
cl_Ball (x,r)) by
Th15;
per cases ;
suppose
A7: t
in (
Sphere (x,r));
take t;
thus thesis by
A2,
A3,
A7,
Th34;
end;
suppose
A8: not t
in (
Sphere (x,r));
A9:
now
assume
A10: X
= t;
((t
+ (
- ((1
/ 2)
* s)))
+ (
- ((1
/ 2)
* t)))
= ((t
- ((1
/ 2)
* s))
- ((1
/ 2)
* t))
.= (t
- t) by
A10,
RLVECT_1: 27
.= (
0. (
TOP-REAL n)) by
RLVECT_1: 5;
then (
0. (
TOP-REAL n))
= ((t
+ (
- ((1
/ 2)
* t)))
+ (
- ((1
/ 2)
* s))) by
RLVECT_1:def 3
.= (((1
* t)
- ((1
/ 2)
* t))
- ((1
/ 2)
* s)) by
RLVECT_1:def 8
.= (((1
- (1
/ 2))
* t)
- ((1
/ 2)
* s)) by
RLVECT_1: 35
.= ((1
/ 2)
* (t
- s)) by
RLVECT_1: 34;
then (t
- s)
= (
0. (
TOP-REAL n)) by
RLVECT_1: 11;
hence contradiction by
A2,
RLVECT_1: 21;
end;
((
Ball (x,r))
\/ (
Sphere (x,r)))
= (
cl_Ball (x,r)) by
Th16;
then
A11: t
in (
Ball (G,r)) by
A4,
A5,
A8,
XBOOLE_0:def 3;
set a = (((
- (2
*
|((t
- X), (X
- x))|))
+ (
sqrt (
delta ((
Sum (
sqr (T
- S))),(2
*
|((t
- X), (X
- x))|),((
Sum (
sqr (S
- Y)))
- (r
^2 ))))))
/ (2
* (
Sum (
sqr (T
- S)))));
A12: ((1
/ 2)
+ (1
/ 2))
= 1 &
|.(1
/ 2).|
= (1
/ 2) by
ABSVALUE:def 1;
(
Ball (G,r))
= (
Ball (x,r)) by
Th11;
then X
in (
Ball (G,r)) by
A3,
A6,
A12,
A11,
Th22;
then
consider e1 be
Point of (
TOP-REAL n) such that
A13:
{e1}
= ((
halfline (X,t))
/\ (
Sphere (x,r))) and
A14: e1
= (((1
- a)
* X)
+ (a
* t)) by
A1,
A5,
A9,
Th35;
take e1;
A15: e1
in
{e1} by
TARSKI:def 1;
then e1
in (
halfline (X,t)) by
A13,
XBOOLE_0:def 4;
then
consider l be
Real such that
A16: e1
= (((1
- l)
* X)
+ (l
* t)) and
A17:
0
<= l;
hereby
assume e1
= s;
then (
0. (
TOP-REAL n))
= ((((1
- l)
* X)
+ (l
* t))
- s) by
A16,
RLVECT_1: 5
.= (((((1
- l)
* ((1
/ 2)
* s))
+ ((1
- l)
* ((1
/ 2)
* t)))
+ (l
* t))
- s) by
RLVECT_1:def 5
.= ((((1
- l)
* ((1
/ 2)
* s))
+ (((1
- l)
* ((1
/ 2)
* t))
+ (l
* t)))
- s) by
RLVECT_1:def 3
.= ((((1
- l)
* ((1
/ 2)
* s))
- s)
+ (((1
- l)
* ((1
/ 2)
* t))
+ (l
* t))) by
RLVECT_1:def 3
.= ((((1
- l)
* ((1
/ 2)
* s))
- (1
* s))
+ (((1
- l)
* ((1
/ 2)
* t))
+ (l
* t))) by
RLVECT_1:def 8
.= (((((1
- l)
* (1
/ 2))
* s)
- (1
* s))
+ (((1
- l)
* ((1
/ 2)
* t))
+ (l
* t))) by
RLVECT_1:def 7
.= (((((1
- l)
* (1
/ 2))
- 1)
* s)
+ (((1
- l)
* ((1
/ 2)
* t))
+ (l
* t))) by
RLVECT_1: 35
.= ((((
- (1
/ 2))
- (l
* (1
/ 2)))
* s)
+ ((((1
- l)
* (1
/ 2))
* t)
+ (l
* t))) by
RLVECT_1:def 7
.= ((((
- (1
/ 2))
- (l
* (1
/ 2)))
* s)
+ ((((1
- l)
* (1
/ 2))
+ l)
* t)) by
RLVECT_1:def 6
.= (((
- ((1
/ 2)
+ (l
* (1
/ 2))))
* s)
+ (((1
/ 2)
+ (l
* (1
/ 2)))
* t))
.= ((((1
/ 2)
+ (l
* (1
/ 2)))
* t)
- (((1
/ 2)
+ (l
* (1
/ 2)))
* s)) by
RLVECT_1: 79
.= (((1
/ 2)
+ (l
* (1
/ 2)))
* (t
- s)) by
RLVECT_1: 34;
then ((1
/ 2)
+ (l
* (1
/ 2)))
=
0 or (t
- s)
= (
0. (
TOP-REAL n)) by
RLVECT_1: 11;
hence contradiction by
A2,
A17,
RLVECT_1: 21;
end;
A18: s
in (
halfline (s,t)) by
Th25;
hereby
set o = ((1
+ l)
/ 2);
let m be
object;
assume m
in
{s, e1};
then
A19: m
= s or m
= e1 by
TARSKI:def 2;
e1
= ((((1
- l)
* ((1
/ 2)
* s))
+ ((1
- l)
* ((1
/ 2)
* t)))
+ (l
* t)) by
A16,
RLVECT_1:def 5
.= (((((1
- l)
* (1
/ 2))
* s)
+ ((1
- l)
* ((1
/ 2)
* t)))
+ (l
* t)) by
RLVECT_1:def 7
.= (((((1
- l)
* (1
/ 2))
* s)
+ (((1
- l)
* (1
/ 2))
* t))
+ (l
* t)) by
RLVECT_1:def 7
.= ((((1
- l)
* (1
/ 2))
* s)
+ ((((1
- l)
* (1
/ 2))
* t)
+ (l
* t))) by
RLVECT_1:def 3
.= ((((1
- l)
* (1
/ 2))
* s)
+ ((((1
- l)
* (1
/ 2))
+ l)
* t)) by
RLVECT_1:def 6
.= (((1
- o)
* s)
+ (o
* t));
then
A20: e1
in (
halfline (s,t)) by
A17;
e1
in (
Sphere (x,r)) by
A13,
A15,
XBOOLE_0:def 4;
hence m
in ((
halfline (s,t))
/\ (
Sphere (x,r))) by
A3,
A18,
A19,
A20,
XBOOLE_0:def 4;
end;
hereby
let m be
object;
assume
A21: m
in ((
halfline (s,t))
/\ (
Sphere (x,r)));
then
A22: m
in (
halfline (s,t)) by
XBOOLE_0:def 4;
A23: m
in (
Sphere (x,r)) by
A21,
XBOOLE_0:def 4;
per cases ;
suppose m
in (
halfline (X,t));
then m
in ((
halfline (X,t))
/\ (
Sphere (x,r))) by
A23,
XBOOLE_0:def 4;
then m
= e1 by
A13,
TARSKI:def 1;
hence m
in
{s, e1} by
TARSKI:def 2;
end;
suppose
A24: not m
in (
halfline (X,t));
consider M be
Real such that
A25: m
= (((1
- M)
* s)
+ (M
* t)) and
A26:
0
<= M by
A22;
A27:
now
set o = ((2
* M)
- 1);
assume M
> 1;
then (2
* M)
> (2
* 1) by
XREAL_1: 68;
then
A28: ((2
* M)
- 1)
> ((2
* 1)
- 1) by
XREAL_1: 14;
(((1
- o)
* X)
+ (o
* t))
= ((((1
- o)
* ((1
/ 2)
* s))
+ ((1
- o)
* ((1
/ 2)
* t)))
+ (o
* t)) by
RLVECT_1:def 5
.= (((((1
- o)
* (1
/ 2))
* s)
+ ((1
- o)
* ((1
/ 2)
* t)))
+ (o
* t)) by
RLVECT_1:def 7
.= (((((1
- o)
* (1
/ 2))
* s)
+ (((1
- o)
* (1
/ 2))
* t))
+ (o
* t)) by
RLVECT_1:def 7
.= ((((1
- o)
* (1
/ 2))
* s)
+ ((((1
- o)
* (1
/ 2))
* t)
+ (o
* t))) by
RLVECT_1:def 3
.= ((((1
- o)
* (1
/ 2))
* s)
+ ((((1
- o)
* (1
/ 2))
+ o)
* t)) by
RLVECT_1:def 6
.= m by
A25;
hence contradiction by
A24,
A28;
end;
|.(t
- x).|
<= r &
|.(t
- x).|
<> r by
A4,
A8,
Th6;
then
|.(t
- x).|
< r by
XXREAL_0: 1;
then t
in (
Ball (x,r));
then
A29: ((
LSeg (s,t))
/\ (
Sphere (x,r)))
=
{s} by
A3,
Th31;
m
in (
LSeg (s,t)) by
A25,
A26,
A27;
then m
in
{s} by
A23,
A29,
XBOOLE_0:def 4;
then m
= s by
TARSKI:def 1;
hence m
in
{s, e1} by
TARSKI:def 2;
end;
end;
thus thesis by
A8,
A14;
end;
end;
registration
let n be
Nat, x be
Point of (
TOP-REAL n);
let r be
negative
Real;
cluster (
Sphere (x,r)) ->
empty;
coherence
proof
assume not thesis;
then
consider y be
Point of (
TOP-REAL n) such that
A1: y
in (
Sphere (x,r));
|.(y
- x).|
= r by
A1,
Th7;
hence contradiction;
end;
end
registration
let n be non
zero
Nat, x be
Point of (
TOP-REAL n);
let r be non
negative
Real;
cluster (
Sphere (x,r)) -> non
empty;
coherence
proof
reconsider e = x as
Point of (
Euclid n) by
TOPREAL3: 8;
per cases ;
suppose r
=
0 ;
then (
Sphere (e,r))
=
{e} by
TOPREAL6: 54;
hence thesis by
Th13;
end;
suppose r
>
0 ;
then
reconsider r as
positive
Real;
consider s be
Point of (
TOP-REAL n) such that
A1: s
in (
Ball (x,r)) by
SUBSET_1: 4;
reconsider S = s, T = (s
+ (
1.REAL n)), XX = x as
Element of (
REAL n) by
EUCLID: 22;
set a = (((
- (2
*
|(((s
+ (
1.REAL n))
- s), (s
- x))|))
+ (
sqrt (
delta ((
Sum (
sqr (T
- S))),(2
*
|(((s
+ (
1.REAL n))
- s), (s
- x))|),((
Sum (
sqr (S
- XX)))
- (r
^2 ))))))
/ (2
* (
Sum (
sqr (T
- S)))));
s
<> (s
+ (
1.REAL n)) by
Th1;
then ex e be
Point of (
TOP-REAL n) st
{e}
= ((
halfline (s,(s
+ (
1.REAL n))))
/\ (
Sphere (x,r))) & e
= (((1
- a)
* s)
+ (a
* (s
+ (
1.REAL n)))) by
A1,
Th35;
hence thesis;
end;
end;
end
theorem ::
TOPREAL9:39
(
Sphere (x,r)) is non
empty implies r
>=
0 ;
theorem ::
TOPREAL9:40
n is non
zero & (
Sphere (x,r)) is
empty implies r
<
0 ;
begin
reserve s,t for
Point of (
TOP-REAL 2);
theorem ::
TOPREAL9:41
(((a
* s)
+ (b
* t))
`1 )
= ((a
* (s
`1 ))
+ (b
* (t
`1 )))
proof
thus (((a
* s)
+ (b
* t))
`1 )
= (((a
* s)
`1 )
+ ((b
* t)
`1 )) by
TOPREAL3: 2
.= ((a
* (s
`1 ))
+ ((b
* t)
`1 )) by
TOPREAL3: 4
.= ((a
* (s
`1 ))
+ (b
* (t
`1 ))) by
TOPREAL3: 4;
end;
theorem ::
TOPREAL9:42
(((a
* s)
+ (b
* t))
`2 )
= ((a
* (s
`2 ))
+ (b
* (t
`2 )))
proof
thus (((a
* s)
+ (b
* t))
`2 )
= (((a
* s)
`2 )
+ ((b
* t)
`2 )) by
TOPREAL3: 2
.= ((a
* (s
`2 ))
+ ((b
* t)
`2 )) by
TOPREAL3: 4
.= ((a
* (s
`2 ))
+ (b
* (t
`2 ))) by
TOPREAL3: 4;
end;
theorem ::
TOPREAL9:43
Th41: t
in (
circle (a,b,r)) iff
|.(t
-
|[a, b]|).|
= r
proof
A1: (
circle (a,b,r))
= { x where x be
Point of (
TOP-REAL 2) :
|.(x
-
|[a, b]|).|
= r } by
JGRAPH_6:def 5;
hereby
assume t
in (
circle (a,b,r));
then ex x be
Point of (
TOP-REAL 2) st t
= x &
|.(x
-
|[a, b]|).|
= r by
A1;
hence
|.(t
-
|[a, b]|).|
= r;
end;
thus thesis by
A1;
end;
theorem ::
TOPREAL9:44
Th42: t
in (
closed_inside_of_circle (a,b,r)) iff
|.(t
-
|[a, b]|).|
<= r
proof
A1: (
closed_inside_of_circle (a,b,r))
= { x where x be
Point of (
TOP-REAL 2) :
|.(x
-
|[a, b]|).|
<= r } by
JGRAPH_6:def 7;
hereby
assume t
in (
closed_inside_of_circle (a,b,r));
then ex x be
Point of (
TOP-REAL 2) st t
= x &
|.(x
-
|[a, b]|).|
<= r by
A1;
hence
|.(t
-
|[a, b]|).|
<= r;
end;
thus thesis by
A1;
end;
theorem ::
TOPREAL9:45
Th43: t
in (
inside_of_circle (a,b,r)) iff
|.(t
-
|[a, b]|).|
< r
proof
A1: (
inside_of_circle (a,b,r))
= { x where x be
Point of (
TOP-REAL 2) :
|.(x
-
|[a, b]|).|
< r } by
JGRAPH_6:def 6;
hereby
assume t
in (
inside_of_circle (a,b,r));
then ex x be
Point of (
TOP-REAL 2) st t
= x &
|.(x
-
|[a, b]|).|
< r by
A1;
hence
|.(t
-
|[a, b]|).|
< r;
end;
thus thesis by
A1;
end;
registration
let a,b be
Real;
let r be
positive
Real;
cluster (
inside_of_circle (a,b,r)) -> non
empty;
coherence
proof
|.(
|[a, b]|
-
|[a, b]|).|
=
0 by
TOPRNS_1: 28;
hence thesis by
Th43;
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
proof
|.(
|[a, b]|
-
|[a, b]|).|
=
0 by
TOPRNS_1: 28;
hence thesis by
Th42;
end;
end
theorem ::
TOPREAL9:46
(
circle (a,b,r))
c= (
closed_inside_of_circle (a,b,r))
proof
let x be
object;
assume
A1: x
in (
circle (a,b,r));
then
reconsider x as
Point of (
TOP-REAL 2);
|.(x
-
|[a, b]|).|
= r by
A1,
Th41;
hence thesis by
Th42;
end;
theorem ::
TOPREAL9:47
Th45: for x be
Point of (
Euclid 2) st x
=
|[a, b]| holds (
cl_Ball (x,r))
= (
closed_inside_of_circle (a,b,r))
proof
let x be
Point of (
Euclid 2) such that
A1: x
=
|[a, b]|;
hereby
let w be
object;
assume
A2: w
in (
cl_Ball (x,r));
then
reconsider u = w as
Point of (
TOP-REAL 2) by
TOPREAL3: 8;
reconsider e = u as
Point of (
Euclid 2) by
TOPREAL3: 8;
(
dist (e,x))
=
|.(u
-
|[a, b]|).| by
A1,
JGRAPH_1: 28;
then
|.(u
-
|[a, b]|).|
<= r by
A2,
METRIC_1: 12;
hence w
in (
closed_inside_of_circle (a,b,r)) by
Th42;
end;
let w be
object;
assume
A3: w
in (
closed_inside_of_circle (a,b,r));
then
reconsider u = w as
Point of (
TOP-REAL 2);
reconsider e = u as
Point of (
Euclid 2) by
TOPREAL3: 8;
(
dist (e,x))
=
|.(u
-
|[a, b]|).| by
A1,
JGRAPH_1: 28;
then (
dist (e,x))
<= r by
A3,
Th42;
hence thesis by
METRIC_1: 12;
end;
theorem ::
TOPREAL9:48
Th46: for x be
Point of (
Euclid 2) st x
=
|[a, b]| holds (
Ball (x,r))
= (
inside_of_circle (a,b,r))
proof
let x be
Point of (
Euclid 2) such that
A1: x
=
|[a, b]|;
hereby
let w be
object;
assume
A2: w
in (
Ball (x,r));
then
reconsider u = w as
Point of (
TOP-REAL 2) by
TOPREAL3: 8;
reconsider e = u as
Point of (
Euclid 2) by
TOPREAL3: 8;
(
dist (e,x))
=
|.(u
-
|[a, b]|).| by
A1,
JGRAPH_1: 28;
then
|.(u
-
|[a, b]|).|
< r by
A2,
METRIC_1: 11;
hence w
in (
inside_of_circle (a,b,r)) by
Th43;
end;
let w be
object;
assume
A3: w
in (
inside_of_circle (a,b,r));
then
reconsider u = w as
Point of (
TOP-REAL 2);
reconsider e = u as
Point of (
Euclid 2) by
TOPREAL3: 8;
(
dist (e,x))
=
|.(u
-
|[a, b]|).| by
A1,
JGRAPH_1: 28;
then (
dist (e,x))
< r by
A3,
Th43;
hence thesis by
METRIC_1: 11;
end;
theorem ::
TOPREAL9:49
Th47: for x be
Point of (
Euclid 2) st x
=
|[a, b]| holds (
Sphere (x,r))
= (
circle (a,b,r))
proof
let x be
Point of (
Euclid 2) such that
A1: x
=
|[a, b]|;
hereby
let w be
object;
assume
A2: w
in (
Sphere (x,r));
then
reconsider u = w as
Point of (
TOP-REAL 2) by
TOPREAL3: 8;
reconsider e = u as
Point of (
Euclid 2) by
TOPREAL3: 8;
(
dist (e,x))
=
|.(u
-
|[a, b]|).| by
A1,
JGRAPH_1: 28;
then
|.(u
-
|[a, b]|).|
= r by
A2,
METRIC_1: 13;
hence w
in (
circle (a,b,r)) by
Th41;
end;
let w be
object;
assume
A3: w
in (
circle (a,b,r));
then
reconsider u = w as
Point of (
TOP-REAL 2);
reconsider e = u as
Point of (
Euclid 2) by
TOPREAL3: 8;
(
dist (e,x))
=
|.(u
-
|[a, b]|).| by
A1,
JGRAPH_1: 28;
then (
dist (e,x))
= r by
A3,
Th41;
hence thesis by
METRIC_1: 13;
end;
theorem ::
TOPREAL9:50
Th48: (
Ball (
|[a, b]|,r))
= (
inside_of_circle (a,b,r))
proof
reconsider e =
|[a, b]| as
Point of (
Euclid 2) by
TOPREAL3: 8;
thus (
Ball (
|[a, b]|,r))
= (
Ball (e,r)) by
Th11
.= (
inside_of_circle (a,b,r)) by
Th46;
end;
theorem ::
TOPREAL9:51
(
cl_Ball (
|[a, b]|,r))
= (
closed_inside_of_circle (a,b,r))
proof
reconsider e =
|[a, b]| as
Point of (
Euclid 2) by
TOPREAL3: 8;
thus (
cl_Ball (
|[a, b]|,r))
= (
cl_Ball (e,r)) by
Th12
.= (
closed_inside_of_circle (a,b,r)) by
Th45;
end;
theorem ::
TOPREAL9:52
Th50: (
Sphere (
|[a, b]|,r))
= (
circle (a,b,r))
proof
reconsider e =
|[a, b]| as
Point of (
Euclid 2) by
TOPREAL3: 8;
thus (
Sphere (
|[a, b]|,r))
= (
Sphere (e,r)) by
Th13
.= (
circle (a,b,r)) by
Th47;
end;
theorem ::
TOPREAL9:53
(
inside_of_circle (a,b,r))
c= (
closed_inside_of_circle (a,b,r))
proof
let x be
object;
assume
A1: x
in (
inside_of_circle (a,b,r));
then
reconsider x as
Point of (
TOP-REAL 2);
|.(x
-
|[a, b]|).|
< r by
A1,
Th43;
hence thesis by
Th42;
end;
theorem ::
TOPREAL9:54
(
inside_of_circle (a,b,r))
misses (
circle (a,b,r))
proof
assume not thesis;
then
consider x be
object such that
A1: x
in (
inside_of_circle (a,b,r)) and
A2: x
in (
circle (a,b,r)) by
XBOOLE_0: 3;
reconsider x as
Point of (
TOP-REAL 2) by
A1;
|.(x
-
|[a, b]|).|
= r by
A2,
Th41;
hence thesis by
A1,
Th43;
end;
theorem ::
TOPREAL9:55
((
inside_of_circle (a,b,r))
\/ (
circle (a,b,r)))
= (
closed_inside_of_circle (a,b,r))
proof
reconsider p =
|[a, b]| as
Point of (
Euclid 2) by
TOPREAL3: 8;
A1: (
cl_Ball (p,r))
= (
closed_inside_of_circle (a,b,r)) by
Th45;
(
Sphere (p,r))
= (
circle (a,b,r)) & (
Ball (p,r))
= (
inside_of_circle (a,b,r)) by
Th46,
Th47;
hence thesis by
A1,
METRIC_1: 16;
end;
theorem ::
TOPREAL9:56
s
in (
Sphere ((
0. (
TOP-REAL 2)),r)) implies (((s
`1 )
^2 )
+ ((s
`2 )
^2 ))
= (r
^2 )
proof
assume s
in (
Sphere ((
0. (
TOP-REAL 2)),r));
then
|.(s
- (
0. (
TOP-REAL 2))).|
= r by
Th7;
then
|.s.|
= r by
RLVECT_1: 13;
hence thesis by
JGRAPH_1: 29;
end;
theorem ::
TOPREAL9:57
s
<> t & s
in (
closed_inside_of_circle (a,b,r)) & t
in (
closed_inside_of_circle (a,b,r)) implies r
>
0
proof
reconsider x =
|[a, b]| as
Point of (
Euclid 2) by
TOPREAL3: 8;
(
cl_Ball (x,r))
= (
closed_inside_of_circle (a,b,r)) by
Th45;
hence thesis by
Th4;
end;
theorem ::
TOPREAL9:58
for S,T,X be
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 be
Point of (
TOP-REAL 2) st
{e}
= ((
halfline (s,t))
/\ (
circle (a,b,r))) & e
= (((1
- w)
* s)
+ (w
* t))
proof
A1: (
Ball (
|[a, b]|,r))
= (
inside_of_circle (a,b,r)) & (
Sphere (
|[a, b]|,r))
= (
circle (a,b,r)) by
Th48,
Th50;
let S,T,X be
Element of (
REAL 2);
assume 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));
hence thesis by
A1,
Th35;
end;
theorem ::
TOPREAL9:59
s
in (
circle (a,b,r)) & t
in (
inside_of_circle (a,b,r)) implies ((
LSeg (s,t))
/\ (
circle (a,b,r)))
=
{s}
proof
assume
A1: s
in (
circle (a,b,r)) & t
in (
inside_of_circle (a,b,r));
reconsider e =
|[a, b]| as
Point of (
Euclid 2) by
TOPREAL3: 8;
A2: (
inside_of_circle (a,b,r))
= (
Ball (e,r)) by
Th46
.= (
Ball (
|[a, b]|,r)) by
Th11;
(
circle (a,b,r))
= (
Sphere (e,r)) by
Th47
.= (
Sphere (
|[a, b]|,r)) by
Th13;
hence thesis by
A1,
A2,
Th31;
end;
theorem ::
TOPREAL9:60
s
in (
circle (a,b,r)) & t
in (
circle (a,b,r)) implies ((
LSeg (s,t))
\
{s, t})
c= (
inside_of_circle (a,b,r))
proof
assume
A1: s
in (
circle (a,b,r)) & t
in (
circle (a,b,r));
reconsider G =
|[a, b]| as
Point of (
Euclid 2) by
TOPREAL3: 8;
(
Sphere (G,r))
= (
circle (a,b,r)) by
Th47;
then
A2: (
Sphere (
|[a, b]|,r))
= (
circle (a,b,r)) by
Th13;
(
Ball (
|[a, b]|,r))
= (
inside_of_circle (a,b,r)) by
Th48;
hence thesis by
A1,
A2,
Th32;
end;
theorem ::
TOPREAL9:61
s
in (
circle (a,b,r)) & t
in (
circle (a,b,r)) implies ((
LSeg (s,t))
/\ (
circle (a,b,r)))
=
{s, t}
proof
reconsider G =
|[a, b]| as
Point of (
Euclid 2) by
TOPREAL3: 8;
(
Sphere (G,r))
= (
circle (a,b,r)) by
Th47;
then
A1: (
Sphere (
|[a, b]|,r))
= (
circle (a,b,r)) by
Th13;
assume s
in (
circle (a,b,r)) & t
in (
circle (a,b,r));
hence thesis by
A1,
Th33;
end;
theorem ::
TOPREAL9:62
s
in (
circle (a,b,r)) & t
in (
circle (a,b,r)) implies ((
halfline (s,t))
/\ (
circle (a,b,r)))
=
{s, t}
proof
assume
A1: s
in (
circle (a,b,r)) & t
in (
circle (a,b,r));
reconsider e =
|[a, b]| as
Point of (
Euclid 2) by
TOPREAL3: 8;
(
circle (a,b,r))
= (
Sphere (e,r)) by
Th47
.= (
Sphere (
|[a, b]|,r)) by
Th13;
hence thesis by
A1,
Th34;
end;
theorem ::
TOPREAL9:63
for S,T,Y be
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 be
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
reconsider G =
|[a, b]| as
Point of (
Euclid 2) by
TOPREAL3: 8;
A1: (
cl_Ball (G,r))
= (
closed_inside_of_circle (a,b,r)) & (
cl_Ball (G,r))
= (
cl_Ball (
|[a, b]|,r)) by
Th12,
Th45;
(
Sphere (G,r))
= (
circle (a,b,r)) by
Th47;
then
A2: (
Sphere (
|[a, b]|,r))
= (
circle (a,b,r)) by
Th13;
let S,T,Y be
Element of (
REAL 2);
assume 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));
hence thesis by
A1,
A2,
Th36;
end;
registration
let a,b,r be
Real;
cluster (
inside_of_circle (a,b,r)) ->
convex;
coherence
proof
(
inside_of_circle (a,b,r))
= { q where q be
Point of (
TOP-REAL 2) :
|.(q
-
|[a, b]|).|
< r } by
JGRAPH_6:def 6;
hence thesis by
Lm2;
end;
cluster (
closed_inside_of_circle (a,b,r)) ->
convex;
coherence
proof
(
closed_inside_of_circle (a,b,r))
= { q where q be
Point of (
TOP-REAL 2) :
|.(q
-
|[a, b]|).|
<= r } by
JGRAPH_6:def 7;
hence thesis by
Lm1;
end;
end
theorem ::
TOPREAL9:64
Th62: for V be
RealLinearSpace, p1,p2 be
Point of V holds (
halfline (p1,p2))
c= (
Line (p1,p2))
proof
let V be
RealLinearSpace, p1,p2 be
Point of V;
let e be
object;
assume e
in (
halfline (p1,p2));
then ex r st e
= (((1
- r)
* p1)
+ (r
* p2)) &
0
<= r;
hence e
in (
Line (p1,p2));
end;
theorem ::
TOPREAL9:65
Th63: for V be
RealLinearSpace, p1,p2 be
Point of V holds (
Line (p1,p2))
= ((
halfline (p1,p2))
\/ (
halfline (p2,p1)))
proof
let V be
RealLinearSpace, p1,p2 be
Point of V;
thus (
Line (p1,p2))
c= ((
halfline (p1,p2))
\/ (
halfline (p2,p1)))
proof
let e be
object;
assume e
in (
Line (p1,p2));
then
consider r such that
A1: e
= (((1
- r)
* p1)
+ (r
* p2));
now
per cases ;
case r
>=
0 ;
hence e
in (
halfline (p1,p2)) by
A1;
end;
case r
<=
0 ;
then
A2: (1
- r)
>=
0 ;
e
= (((1
- (1
- r))
* p2)
+ ((1
- r)
* p1)) by
A1;
hence e
in (
halfline (p2,p1)) by
A2;
end;
end;
hence thesis by
XBOOLE_0:def 3;
end;
(
halfline (p1,p2))
c= (
Line (p1,p2)) & (
halfline (p2,p1))
c= (
Line (p1,p2)) by
Th62;
hence thesis by
XBOOLE_1: 8;
end;
theorem ::
TOPREAL9:66
Th64: for V be
RealLinearSpace, p1,p2,p3 be
Point of V st p1
in (
halfline (p2,p3)) holds p1
in (
LSeg (p2,p3)) or p3
in (
LSeg (p2,p1))
proof
let V be
RealLinearSpace, p1,p2,p3 be
Point of V;
assume p1
in (
halfline (p2,p3));
then
consider r such that
A1: p1
= (((1
- r)
* p2)
+ (r
* p3)) and
A2:
0
<= r;
set s = (1
/ r);
now
per cases ;
case r
<= 1;
hence p1
in (
LSeg (p2,p3)) by
A1,
A2;
end;
case
A3: r
>= 1;
per cases by
A2;
case r
=
0 ;
then p1
= p2 by
A1,
Th2;
hence p1
in (
LSeg (p2,p3)) by
RLTOPSP1: 68;
end;
case
A4: r
>
0 ;
then
A5: (s
* r)
= 1 by
XCMPLX_1: 87;
A6: s
<= 1 by
A3,
XREAL_1: 183;
A7: (r
* p3)
= (p1
- ((1
- r)
* p2)) by
RLVECT_4: 1,
A1;
((s
* r)
* p3)
= (s
* (r
* p3)) by
RLVECT_1:def 7
.= ((s
* p1)
- (s
* ((1
- r)
* p2))) by
RLVECT_1: 34,
A7
.= ((s
* p1)
- ((s
* (1
- r))
* p2)) by
RLVECT_1:def 7;
then p3
= ((s
* p1)
- ((s
* (1
- r))
* p2)) by
RLVECT_1:def 8,
A5
.= ((s
* p1)
+ ((
- (s
* (1
- r)))
* p2)) by
RLVECT_1: 79
.= ((s
* p1)
+ ((1
- s)
* p2)) by
A5;
hence p3
in (
LSeg (p2,p1)) by
A4,
A6;
end;
end;
end;
hence thesis;
end;
theorem ::
TOPREAL9:67
for V be
RealLinearSpace, p1,p2,p3 be
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
let V be
RealLinearSpace, p1,p2,p3 be
Point of V;
thus (p1,p2,p3)
are_collinear implies p1
in (
LSeg (p2,p3)) or p2
in (
LSeg (p3,p1)) or p3
in (
LSeg (p1,p2))
proof
assume (p1,p2,p3)
are_collinear ;
then
consider L be
line of V such that
A1: p1
in L and
A2: p2
in L and
A3: p3
in L;
consider x1,x2 be
Point of V such that
A4: L
= (
Line (x1,x2)) by
RLTOPSP1:def 15;
per cases ;
suppose p2
= p3;
hence thesis by
RLTOPSP1: 68;
end;
suppose p2
<> p3;
then
A5: (
Line (p2,p3))
= L by
A2,
A3,
RLTOPSP1: 75,
A4;
per cases ;
suppose p1
in (
halfline (p2,p3));
hence thesis by
Th64;
end;
suppose
A6: not p1
in (
halfline (p2,p3));
L
= ((
halfline (p2,p3))
\/ (
halfline (p3,p2))) by
Th63,
A5;
then p1
in (
halfline (p3,p2)) by
A1,
XBOOLE_0:def 3,
A6;
hence thesis by
Th64;
end;
end;
end;
assume p1
in (
LSeg (p2,p3)) or p2
in (
LSeg (p3,p1)) or p3
in (
LSeg (p1,p2));
per cases ;
suppose
A7: p1
in (
LSeg (p2,p3));
take (
Line (p2,p3));
(
LSeg (p2,p3))
c= (
Line (p2,p3)) by
RLTOPSP1: 73;
hence p1
in (
Line (p2,p3)) by
A7;
thus p2
in (
Line (p2,p3)) by
RLTOPSP1: 72;
thus p3
in (
Line (p2,p3)) by
RLTOPSP1: 72;
end;
suppose
A8: p2
in (
LSeg (p3,p1));
take (
Line (p3,p1));
thus p1
in (
Line (p3,p1)) by
RLTOPSP1: 72;
(
LSeg (p3,p1))
c= (
Line (p3,p1)) by
RLTOPSP1: 73;
hence p2
in (
Line (p3,p1)) by
A8;
thus p3
in (
Line (p3,p1)) by
RLTOPSP1: 72;
end;
suppose
A9: p3
in (
LSeg (p1,p2));
take (
Line (p1,p2));
thus p1
in (
Line (p1,p2)) by
RLTOPSP1: 72;
thus p2
in (
Line (p1,p2)) by
RLTOPSP1: 72;
(
LSeg (p1,p2))
c= (
Line (p1,p2)) by
RLTOPSP1: 73;
hence p3
in (
Line (p1,p2)) by
A9;
end;
end;