---

Step * of Lemma sub-cube_wf

∀[k:ℕ]. ∀[up:ℕk ⟶ 𝔹]. ∀[c:real-cube(k)].  (sub-cube(up;c) ∈ real-cube(k))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[up:\mBbbN{}k  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[c:real-cube(k)].    (sub-cube(up;c)  \mmember{}  real-cube(k))


By

---

Latex:
Auto

---

Home Index