---

Step * of Lemma mu-bound-property

∀[b:ℕ]. ∀[f:ℕb ⟶ 𝔹].  {(↑(f mu(f))) ∧ (∀[i:ℕb]. ¬↑(f i) supposing i < mu(f))} supposing ∃n:ℕb. (↑(f n))
BY
{ (Intros THEN (Assert mu(f) ∈ ℕb BY (BLemma `mu-bound` THEN Auto)) THEN Unfold `guard` 0 THEN (Unhide THENA Auto)) }

1
1. [b] : ℕ
2. [f] : ℕb ⟶ 𝔹
3. [%] : ∃n:ℕb. (↑(f n))
4. mu(f) ∈ ℕb
⊢ SqStable(↑(f mu(f)))

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

---

Latex:

---

Latex:
\mforall{}[b:\mBbbN{}].  \mforall{}[f:\mBbbN{}b  {}\mrightarrow{}  \mBbbB{}].
    \{(\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:
(Intros
  THEN  (Assert  mu(f)  \mmember{}  \mBbbN{}b  BY
                          (BLemma  `mu-bound`  THEN  Auto))
  THEN  Unfold  `guard`  0
  THEN  (Unhide  THENA  Auto))

---

Home Index