---

Step * of Lemma real-ball-coordinate-range

∀[r:{r:ℝ| r0 ≤ r} ]. ∀[n:ℕ]. ∀[i:ℕn]. ∀[x:B(n;r)].  (x i ∈ [-(r), r])
BY
{ (Auto THEN (Unhide THENL [(Reduce 0 THEN Auto); D -1]) THEN (Unhide THENA Auto)) }

1
1. r : {r:ℝ| r0 ≤ r} 
2. n : ℕ
3. i : ℕn
4. x : ℝ^n
5. ||x|| ≤ r
⊢ x i ∈ [-(r), r]

---

Latex:

---

Latex:
\mforall{}[r:\{r:\mBbbR{}|  r0  \mleq{}  r\}  ].  \mforall{}[n:\mBbbN{}].  \mforall{}[i:\mBbbN{}n].  \mforall{}[x:B(n;r)].    (x  i  \mmember{}  [-(r),  r])


By

---

Latex:
(Auto  THEN  (Unhide  THENL  [(Reduce  0  THEN  Auto);  D  -1])  THEN  (Unhide  THENA  Auto))

---

Home Index