let n be Nat; :: thesis: 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
let a be Real; :: thesis: 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
let P be Subset of (TOP-REAL n); :: thesis: 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
let Q be Point of (TOP-REAL n); :: thesis: ( P = { q where q is Point of (TOP-REAL n) : |.(q - Q).| < a } implies P is convex )
assume A1: P = { q where q is Point of (TOP-REAL n) : |.(q - Q).| < a } ; :: thesis: P is convex
reconsider e = Q as Point of (Euclid n) by TOPREAL3:8;
let p1, p2 be Point of (TOP-REAL n); :: according to JORDAN1:def 1 :: thesis: ( not p1 in P or not p2 in P or LSeg (p1,p2) c= P )
assume A2: ( p1 in P & p2 in P ) ; :: thesis: LSeg (p1,p2) c= P
Ball (e,a) = Ball (Q,a) by Th11
.= P by A1 ;
hence LSeg (p1,p2) c= P by A2, TOPREAL3:21; :: thesis: verum