---

Step * of Lemma partition-choice-subtype

∀[p:ℝ List]. ({f:ℕ||p|| - 1 ⟶ ℝ| is-partition-choice(p;f)}  ⊆r partition-choice(p))
BY
{ ((Auto THEN (D 0 THENA Auto))
   THEN D -1
   THEN Unfold `partition-choice` 0
   THEN ExtWith [`i'] [⌜ℕ||p|| - 1 ⟶ ℝ⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[p:\mBbbR{}  List].  (\{f:\mBbbN{}||p||  -  1  {}\mrightarrow{}  \mBbbR{}|  is-partition-choice(p;f)\}    \msubseteq{}r  partition-choice(p))


By

---

Latex:
((Auto  THEN  (D  0  THENA  Auto))
  THEN  D  -1
  THEN  Unfold  `partition-choice`  0
  THEN  ExtWith  [`i']  [\mkleeneopen{}\mBbbN{}||p||  -  1  {}\mrightarrow{}  \mBbbR{}\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index