let a be Real; for P being Subset of (TOP-REAL 1) st P = { q where q is Point of (TOP-REAL 1) : ex r being Real st
( q = <*r*> & r < - a ) } holds
P is convex
let P be Subset of (TOP-REAL 1); ( P = { q where q is Point of (TOP-REAL 1) : ex r being Real st
( q = <*r*> & r < - a ) } implies P is convex )
assume A1:
P = { q where q is Point of (TOP-REAL 1) : ex r being Real st
( q = <*r*> & r < - a ) }
; P is convex
for w1, w2 being Point of (TOP-REAL 1) st w1 in P & w2 in P holds
LSeg (w1,w2) c= P
proof
let w1,
w2 be
Point of
(TOP-REAL 1);
( w1 in P & w2 in P implies LSeg (w1,w2) c= P )
assume that A2:
w1 in P
and A3:
w2 in P
;
LSeg (w1,w2) c= P
consider q2 being
Point of
(TOP-REAL 1) such that A4:
q2 = w2
and A5:
ex
r being
Real st
(
q2 = <*r*> &
r < - a )
by A1, A3;
consider q1 being
Point of
(TOP-REAL 1) such that A6:
q1 = w1
and A7:
ex
r being
Real st
(
q1 = <*r*> &
r < - a )
by A1, A2;
consider r2 being
Real such that A8:
q2 = <*r2*>
and A9:
r2 < - a
by A5;
consider r1 being
Real such that A10:
q1 = <*r1*>
and A11:
r1 < - a
by A7;
thus
LSeg (
w1,
w2)
c= P
verumproof
let x be
object ;
TARSKI:def 3 ( not x in LSeg (w1,w2) or x in P )
assume
x in LSeg (
w1,
w2)
;
x in P
then consider r3 being
Real such that A12:
x = ((1 - r3) * w1) + (r3 * w2)
and A13:
0 <= r3
and A14:
r3 <= 1
;
A15:
1
- r3 >= 0
by A14, XREAL_1:48;
per cases
( r3 > 0 or r3 <= 0 )
;
suppose A16:
r3 > 0
;
x in PA17:
(
(1 - r3) * r1 <= (1 - r3) * (- a) &
((1 - r3) * (- a)) + (r3 * (- a)) = - a )
by A11, A15, XREAL_1:64;
r3 * r2 < r3 * (- a)
by A9, A16, XREAL_1:68;
then A18:
((1 - r3) * r1) + (r3 * r2) < - a
by A17, XREAL_1:8;
<*(((1 - r3) * r1) + (r3 * r2))*> =
|[((1 - r3) * r1)]| + |[(r3 * r2)]|
by JORDAN2B:22
.=
((1 - r3) * |[r1]|) + |[(r3 * r2)]|
by JORDAN2B:21
.=
((1 - r3) * |[r1]|) + (r3 * |[r2]|)
by JORDAN2B:21
;
hence
x in P
by A1, A6, A10, A4, A8, A12, A18;
verum end; end;
end;
end;
hence
P is convex
by JORDAN1:def 1; verum