---

Step * 1 of Lemma mu-wf2

.....antecedent..... 
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]
⊢ ∃m:{0...}. (↑isl(d m))
BY
{ TACTIC:ParallelLast }

1
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 : ℕ
5. P[n]
⊢ ↑isl(d n)

---

Latex:

---

Latex:
.....antecedent..... 
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]
\mvdash{}  \mexists{}m:\{0...\}.  (\muparrow{}isl(d  m))


By

---

Latex:
TACTIC:ParallelLast

---

Home Index