---

Step * of Lemma assert-fset-minimal

∀[T:Type]. ∀[less:T ⟶ T ⟶ 𝔹]. ∀[s:fset(T)]. ∀[a:T].  uiff(↑fset-minimal(x,y.less[x;y];s;a);fset-all(s;y.¬bless[y;a]))
BY
{ (RepUR ``fset-all fset-minimal`` 0 THEN Auto THEN NthHypEq (-1) THEN RepeatFor 3 ((EqCD THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[less:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[s:fset(T)].  \mforall{}[a:T].
    uiff(\muparrow{}fset-minimal(x,y.less[x;y];s;a);fset-all(s;y.\mneg{}\msubb{}less[y;a]))


By

---

Latex:
(RepUR  ``fset-all  fset-minimal``  0  THEN  Auto  THEN  NthHypEq  (-1)  THEN  RepeatFor  3  ((EqCD  THEN  Auto)))

---

Home Index