let n be Nat; :: thesis: for b being Element of REAL n
for p being Point of (TOP-REAL n) ex a being Element of REAL n st
( a = p & ClosedHypercube (p,b) = ClosedHyperInterval ((a - b),(a + b)) )
let b be Element of REAL n; :: thesis: for p being Point of (TOP-REAL n) ex a being Element of REAL n st
( a = p & ClosedHypercube (p,b) = ClosedHyperInterval ((a - b),(a + b)) )
let p be Point of (TOP-REAL n); :: thesis: ex a being Element of REAL n st
( a = p & ClosedHypercube (p,b) = ClosedHyperInterval ((a - b),(a + b)) )
reconsider a = p as Element of REAL n by EUCLID:22;
take a ; :: thesis: ( a = p & ClosedHypercube (p,b) = ClosedHyperInterval ((a - b),(a + b)) )
thus a = p ; :: thesis: ClosedHypercube (p,b) = ClosedHyperInterval ((a - b),(a + b))
A1: ClosedHypercube (p,b) c= ClosedHyperInterval ((a - b),(a + b))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ClosedHypercube (p,b) or x in ClosedHyperInterval ((a - b),(a + b)) )
assume A2: x in ClosedHypercube (p,b) ; :: thesis: x in ClosedHyperInterval ((a - b),(a + b))
then reconsider y = x as Element of REAL n by EUCLID:22;
for i being Nat st i in Seg n holds
y . i in [.((a - b) . i),((a + b) . i).]
proof
let i be Nat; :: thesis: ( i in Seg n implies y . i in [.((a - b) . i),((a + b) . i).] )
assume A3: i in Seg n ; :: thesis: y . i in [.((a - b) . i),((a + b) . i).]
( (a . i) - (b . i) = (a - b) . i & (a + b) . i = (a . i) + (b . i) ) by RVSUM_1:11, RVSUM_1:27;
hence y . i in [.((a - b) . i),((a + b) . i).] by A2, A3, TIETZE_2:def 2; :: thesis: verum
end;
hence x in ClosedHyperInterval ((a - b),(a + b)) by Def3; :: thesis: verum
end;
ClosedHyperInterval ((a - b),(a + b)) c= ClosedHypercube (p,b)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ClosedHyperInterval ((a - b),(a + b)) or x in ClosedHypercube (p,b) )
assume A4: x in ClosedHyperInterval ((a - b),(a + b)) ; :: thesis: x in ClosedHypercube (p,b)
then reconsider q = x as Element of (TOP-REAL n) by EUCLID:22;
now :: thesis: for i being Nat st i in Seg n holds
q . i in [.((p . i) - (b . i)),((p . i) + (b . i)).]
let i be Nat; :: thesis: ( i in Seg n implies q . i in [.((p . i) - (b . i)),((p . i) + (b . i)).] )
assume A5: i in Seg n ; :: thesis: q . i in [.((p . i) - (b . i)),((p . i) + (b . i)).]
consider y being Element of REAL n such that
A6: x = y and
A7: for i being Nat st i in Seg n holds
y . i in [.((a - b) . i),((a + b) . i).] by A4, Def3;
( (a - b) . i = (a . i) - (b . i) & (a + b) . i = (a . i) + (b . i) ) by RVSUM_1:11, RVSUM_1:27;
hence q . i in [.((p . i) - (b . i)),((p . i) + (b . i)).] by A5, A6, A7; :: thesis: verum
end;
hence x in ClosedHypercube (p,b) by TIETZE_2:def 2; :: thesis: verum
end;
hence ClosedHypercube (p,b) = ClosedHyperInterval ((a - b),(a + b)) by A1; :: thesis: verum