---

Step * 2 of Lemma mu-wf2


1. ∀[f:{0...} ⟶ (Top + Top)]. mu-ge(f;0) ∈ {0...} supposing ∃m:{0...}. (↑isl(f m))
2. P : ℕ ⟶ ℙ
3. d : ∀n:ℕ. Dec(P[n])
4. ∃n:ℕ. P[n]
5. mu(d) ∈ {0...}
⊢ mu(d) ∈ ℕ
BY
{ TACTIC:Auto }

---

Latex:

---

Latex:

1.  \mforall{}[f:\{0...\}  {}\mrightarrow{}  (Top  +  Top)].  mu-ge(f;0)  \mmember{}  \{0...\}  supposing  \mexists{}m:\{0...\}.  (\muparrow{}isl(f  m))
2.  P  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
3.  d  :  \mforall{}n:\mBbbN{}.  Dec(P[n])
4.  \mexists{}n:\mBbbN{}.  P[n]
5.  mu(d)  \mmember{}  \{0...\}
\mvdash{}  mu(d)  \mmember{}  \mBbbN{}


By

---

Latex:
TACTIC:Auto

---

Home Index