---

Step * of Lemma rat-cube-sub-complex-polyhedron-subtype

∀[k:ℕ]. ∀[K:ℚCube(k) List]. ∀[P:{c:ℚCube(k)| (c ∈ K)}  ⟶ 𝔹].  (|rat-cube-sub-complex(P;K)| ⊆r |K|)
BY
{ ((Auto THEN Unfold `rat-cube-sub-complex` 0) THEN BLemma `rat-cube-complex-polyhedron-subtype` THEN Auto) }

1
1. k : ℕ
2. K : ℚCube(k) List
3. P : {c:ℚCube(k)| (c ∈ K)}  ⟶ 𝔹
⊢ filter(P;K) ⊆ K

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[K:\mBbbQ{}Cube(k)  List].  \mforall{}[P:\{c:\mBbbQ{}Cube(k)|  (c  \mmember{}  K)\}    {}\mrightarrow{}  \mBbbB{}].    (|rat-cube-sub-complex(P;K)|  \msubseteq{}r  |K|)


By

---

Latex:
((Auto  THEN  Unfold  `rat-cube-sub-complex`  0)
  THEN  BLemma  `rat-cube-complex-polyhedron-subtype`
  THEN  Auto)

---

Home Index