let n be Nat; for r being Real
for e being Point of (Euclid n) holds Ball (e,r) c= OpenHypercube (e,r)
let r be Real; for e being Point of (Euclid n) holds Ball (e,r) c= OpenHypercube (e,r)
let e be Point of (Euclid n); Ball (e,r) c= OpenHypercube (e,r)
let g be object ; TARSKI:def 3 ( not g in Ball (e,r) or g in OpenHypercube (e,r) )
assume A1:
g in Ball (e,r)
; g in OpenHypercube (e,r)
then reconsider g = g as Point of (Euclid n) ;
A2:
dom (Intervals (e,r)) = dom e
by Def3;
A3:
( dom g = Seg n & dom e = Seg n )
by FINSEQ_1:89;
now for x being object st x in dom (Intervals (e,r)) holds
g . x in (Intervals (e,r)) . xlet x be
object ;
( x in dom (Intervals (e,r)) implies g . x in (Intervals (e,r)) . x )reconsider u =
e . x,
v =
g . x as
Real ;
assume A4:
x in dom (Intervals (e,r))
;
g . x in (Intervals (e,r)) . xthen A5:
(Intervals (e,r)) . x = ].(u - r),(u + r).[
by A2, Def3;
dom (g - e) = (dom g) /\ (dom e)
by VALUED_1:12;
then A6:
(g - e) . x = v - u
by A2, A3, A4, VALUED_1:13;
A7:
v = u + (v - u)
;
|.((g - e) . x).| < r
by A1, Th10;
hence
g . x in (Intervals (e,r)) . x
by A6, A5, A7, FCONT_3:3;
verum end;
hence
g in OpenHypercube (e,r)
by A2, A3, CARD_3:9; verum