let n be Nat; :: thesis: for p being Point of (TOP-REAL n)
for R being real-valued FinSequence st ex i being Nat st
( i in (Seg n) /\ (dom R) & R . i < 0 ) holds
ClosedHypercube (p,R) is empty
let p be Point of (TOP-REAL n); :: thesis: for R being real-valued FinSequence st ex i being Nat st
( i in (Seg n) /\ (dom R) & R . i < 0 ) holds
ClosedHypercube (p,R) is empty
let R be real-valued FinSequence; :: thesis: ( ex i being Nat st
( i in (Seg n) /\ (dom R) & R . i < 0 ) implies ClosedHypercube (p,R) is empty )
given i being Nat such that A1: i in (Seg n) /\ (dom R) and
A2: R . i < 0 ; :: thesis: ClosedHypercube (p,R) is empty
assume not ClosedHypercube (p,R) is empty ; :: thesis: contradiction
then consider x being object such that
A3: x in ClosedHypercube (p,R) ;
reconsider x = x as Point of (TOP-REAL n) by A3;
i in Seg n by A1, XBOOLE_0:def 4;
then A4: x . i in [.((p . i) - (R . i)),((p . i) + (R . i)).] by Def2, A3;
then A5: x . i <= (p . i) + (R . i) by XXREAL_1:1;
(p . i) - (R . i) <= x . i by A4, XXREAL_1:1;
then (p . i) + (- (R . i)) <= (p . i) + (R . i) by A5, XXREAL_0:2;
hence contradiction by A2, XREAL_1:8; :: thesis: verum