---

Step * of Lemma mu-bound-property+

∀[b:ℕ]. ∀[f:ℕb ⟶ 𝔹].  {(mu(f) ∈ ℕb) ∧ (↑(f mu(f))) ∧ (∀[i:ℕb]. ¬↑(f i) supposing i < mu(f))} supposing ∃n:ℕb. (↑(f n))
BY
{ (BasicUniformUnivCD Auto THEN (InstLemma `mu-bound-property` [⌜b⌝; ⌜f⌝])⋅ THEN Auto THEN D 0) }

1
1. [b] : ℕ
2. [f] : ℕb ⟶ 𝔹
3. [%] : ∃n:ℕb. (↑(f n))
4. ↑(f mu(f))
5. ∀[i:ℕb]. ¬↑(f i) supposing i < mu(f)
⊢ mu(f) ∈ ℕb

2
1. [b] : ℕ
2. [f] : ℕb ⟶ 𝔹
3. [%] : ∃n:ℕb. (↑(f n))
4. ↑(f mu(f))
5. ∀[i:ℕb]. ¬↑(f i) supposing i < mu(f)
⊢ (↑(f mu(f))) ∧ (∀[i:ℕb]. ¬↑(f i) supposing i < mu(f))

---

Latex:

---

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


By

---

Latex:
(BasicUniformUnivCD  Auto  THEN  (InstLemma  `mu-bound-property`  [\mkleeneopen{}b\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{}])\mcdot{}  THEN  Auto  THEN  D  0)

---

Home Index