---

Step * of Lemma mu-bound

∀[b:ℕ]. ∀[f:ℕb ⟶ 𝔹].  mu(f) ∈ ℕb supposing ∃n:ℕb. (↑(f n))
BY
{ ((D 0 THENA Auto) THEN ((InstLemma `mu-ge-bound` [⌜0⌝;⌜b⌝]⋅ THENA Auto) THEN Fold `mu` (-1) THEN Auto)) }

---

Latex:

---

Latex:
\mforall{}[b:\mBbbN{}].  \mforall{}[f:\mBbbN{}b  {}\mrightarrow{}  \mBbbB{}].    mu(f)  \mmember{}  \mBbbN{}b  supposing  \mexists{}n:\mBbbN{}b.  (\muparrow{}(f  n))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  ((InstLemma  `mu-ge-bound`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  Fold  `mu`  (-1)  THEN  Auto)
  )

---

Home Index