let a, r, s be Real; ( r <= s implies for p being Point of (Closed-Interval-MSpace (r,s)) holds
( Ball (p,a) = [.r,s.] or Ball (p,a) = [.r,(p + a).[ or Ball (p,a) = ].(p - a),s.] or Ball (p,a) = ].(p - a),(p + a).[ ) )
set M = Closed-Interval-MSpace (r,s);
assume
r <= s
; for p being Point of (Closed-Interval-MSpace (r,s)) holds
( Ball (p,a) = [.r,s.] or Ball (p,a) = [.r,(p + a).[ or Ball (p,a) = ].(p - a),s.] or Ball (p,a) = ].(p - a),(p + a).[ )
then A1:
the carrier of (Closed-Interval-MSpace (r,s)) = [.r,s.]
by TOPMETR:10;
let p be Point of (Closed-Interval-MSpace (r,s)); ( Ball (p,a) = [.r,s.] or Ball (p,a) = [.r,(p + a).[ or Ball (p,a) = ].(p - a),s.] or Ball (p,a) = ].(p - a),(p + a).[ )
set B = Ball (p,a);
reconsider p1 = p as Point of RealSpace by TOPMETR:8;
set B1 = Ball (p1,a);
A2:
Ball (p,a) = (Ball (p1,a)) /\ the carrier of (Closed-Interval-MSpace (r,s))
by TOPMETR:9;
A3:
Ball (p1,a) = ].(p1 - a),(p1 + a).[
by FRECHET:7;
per cases
( ( p1 + a <= s & p1 - a < r ) or ( p1 + a <= s & p1 - a >= r ) or ( p1 + a > s & p1 - a < r ) or ( p1 + a > s & p1 - a >= r ) )
;
suppose that A4:
p1 + a <= s
and A5:
p1 - a < r
;
( Ball (p,a) = [.r,s.] or Ball (p,a) = [.r,(p + a).[ or Ball (p,a) = ].(p - a),s.] or Ball (p,a) = ].(p - a),(p + a).[ )
Ball (
p,
a)
= [.r,(p1 + a).[
proof
thus
Ball (
p,
a)
c= [.r,(p1 + a).[
XBOOLE_0:def 10 [.r,(p1 + a).[ c= Ball (p,a)proof
let b be
object ;
TARSKI:def 3 ( not b in Ball (p,a) or b in [.r,(p1 + a).[ )
assume A6:
b in Ball (
p,
a)
;
b in [.r,(p1 + a).[
then reconsider b =
b as
Element of
Ball (
p,
a) ;
b in Ball (
p1,
a)
by A2, A6, XBOOLE_0:def 4;
then A7:
b < p1 + a
by A3, XXREAL_1:4;
r <= b
by A1, A6, XXREAL_1:1;
hence
b in [.r,(p1 + a).[
by A7, XXREAL_1:3;
verum
end;
let b be
object ;
TARSKI:def 3 ( not b in [.r,(p1 + a).[ or b in Ball (p,a) )
assume A8:
b in [.r,(p1 + a).[
;
b in Ball (p,a)
then reconsider b =
b as
Real ;
A9:
r <= b
by A8, XXREAL_1:3;
A10:
b < p1 + a
by A8, XXREAL_1:3;
then
b <= s
by A4, XXREAL_0:2;
then A11:
b in [.r,s.]
by A9, XXREAL_1:1;
p1 - a < b
by A5, A9, XXREAL_0:2;
then
b in Ball (
p1,
a)
by A3, A10, XXREAL_1:4;
hence
b in Ball (
p,
a)
by A1, A2, A11, XBOOLE_0:def 4;
verum
end; hence
(
Ball (
p,
a)
= [.r,s.] or
Ball (
p,
a)
= [.r,(p + a).[ or
Ball (
p,
a)
= ].(p - a),s.] or
Ball (
p,
a)
= ].(p - a),(p + a).[ )
;
verum end; suppose that A12:
p1 + a <= s
and A13:
p1 - a >= r
;
( Ball (p,a) = [.r,s.] or Ball (p,a) = [.r,(p + a).[ or Ball (p,a) = ].(p - a),s.] or Ball (p,a) = ].(p - a),(p + a).[ )
Ball (
p,
a)
= ].(p1 - a),(p1 + a).[
proof
thus
Ball (
p,
a)
c= ].(p1 - a),(p1 + a).[
by A2, A3, XBOOLE_1:17;
XBOOLE_0:def 10 ].(p1 - a),(p1 + a).[ c= Ball (p,a)
let b be
object ;
TARSKI:def 3 ( not b in ].(p1 - a),(p1 + a).[ or b in Ball (p,a) )
assume A14:
b in ].(p1 - a),(p1 + a).[
;
b in Ball (p,a)
then reconsider b =
b as
Real ;
b < p1 + a
by A14, XXREAL_1:4;
then A15:
b <= s
by A12, XXREAL_0:2;
p1 - a <= b
by A14, XXREAL_1:4;
then
r <= b
by A13, XXREAL_0:2;
then
b in [.r,s.]
by A15, XXREAL_1:1;
hence
b in Ball (
p,
a)
by A1, A2, A3, A14, XBOOLE_0:def 4;
verum
end; hence
(
Ball (
p,
a)
= [.r,s.] or
Ball (
p,
a)
= [.r,(p + a).[ or
Ball (
p,
a)
= ].(p - a),s.] or
Ball (
p,
a)
= ].(p - a),(p + a).[ )
;
verum end; suppose that A16:
p1 + a > s
and A17:
p1 - a < r
;
( Ball (p,a) = [.r,s.] or Ball (p,a) = [.r,(p + a).[ or Ball (p,a) = ].(p - a),s.] or Ball (p,a) = ].(p - a),(p + a).[ )
Ball (
p,
a)
= [.r,s.]
proof
thus
Ball (
p,
a)
c= [.r,s.]
by A1;
XBOOLE_0:def 10 [.r,s.] c= Ball (p,a)
let b be
object ;
TARSKI:def 3 ( not b in [.r,s.] or b in Ball (p,a) )
assume A18:
b in [.r,s.]
;
b in Ball (p,a)
then reconsider b =
b as
Real ;
b <= s
by A18, XXREAL_1:1;
then A19:
b < p1 + a
by A16, XXREAL_0:2;
r <= b
by A18, XXREAL_1:1;
then
p1 - a < b
by A17, XXREAL_0:2;
then
b in Ball (
p1,
a)
by A3, A19, XXREAL_1:4;
hence
b in Ball (
p,
a)
by A1, A2, A18, XBOOLE_0:def 4;
verum
end; hence
(
Ball (
p,
a)
= [.r,s.] or
Ball (
p,
a)
= [.r,(p + a).[ or
Ball (
p,
a)
= ].(p - a),s.] or
Ball (
p,
a)
= ].(p - a),(p + a).[ )
;
verum end; suppose that A20:
p1 + a > s
and A21:
p1 - a >= r
;
( Ball (p,a) = [.r,s.] or Ball (p,a) = [.r,(p + a).[ or Ball (p,a) = ].(p - a),s.] or Ball (p,a) = ].(p - a),(p + a).[ )
Ball (
p,
a)
= ].(p1 - a),s.]
proof
thus
Ball (
p,
a)
c= ].(p1 - a),s.]
XBOOLE_0:def 10 ].(p1 - a),s.] c= Ball (p,a)proof
let b be
object ;
TARSKI:def 3 ( not b in Ball (p,a) or b in ].(p1 - a),s.] )
assume A22:
b in Ball (
p,
a)
;
b in ].(p1 - a),s.]
then reconsider b =
b as
Element of
Ball (
p,
a) ;
b in Ball (
p1,
a)
by A2, A22, XBOOLE_0:def 4;
then A23:
p1 - a < b
by A3, XXREAL_1:4;
b <= s
by A1, A22, XXREAL_1:1;
hence
b in ].(p1 - a),s.]
by A23, XXREAL_1:2;
verum
end;
let b be
object ;
TARSKI:def 3 ( not b in ].(p1 - a),s.] or b in Ball (p,a) )
assume A24:
b in ].(p1 - a),s.]
;
b in Ball (p,a)
then reconsider b =
b as
Real ;
A25:
b <= s
by A24, XXREAL_1:2;
A26:
p1 - a < b
by A24, XXREAL_1:2;
then
r <= b
by A21, XXREAL_0:2;
then A27:
b in [.r,s.]
by A25, XXREAL_1:1;
b < p1 + a
by A20, A25, XXREAL_0:2;
then
b in Ball (
p1,
a)
by A3, A26, XXREAL_1:4;
hence
b in Ball (
p,
a)
by A1, A2, A27, XBOOLE_0:def 4;
verum
end; hence
(
Ball (
p,
a)
= [.r,s.] or
Ball (
p,
a)
= [.r,(p + a).[ or
Ball (
p,
a)
= ].(p - a),s.] or
Ball (
p,
a)
= ].(p - a),(p + a).[ )
;
verum end; end;