---

Step * of Lemma sq_stable__is-partition-choice

∀[p:ℝ List]. ∀[x:ℕ||p|| - 1 ⟶ ℝ].  SqStable(is-partition-choice(p;x))
BY
{ (Auto THEN Unfold `is-partition-choice` 0 THEN Auto THEN RepUR ``i-member`` 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Unfold  `is-partition-choice`  0  THEN  Auto  THEN  RepUR  ``i-member``  0  THEN  Auto)

---

Home Index