---

Step * of Lemma unary-strong-almost-full-has-strict-inc

∀[A:ℕ ⟶ ℙ]. ((∀s:StrictInc. ∃n:ℕ. A[s n]) ⇒ (∃s:StrictInc. ∀n:ℕ. A[s n]))
BY
{ (Auto THEN Assert ⌜∀m:ℕ. ∃n:ℕ. (m < n ∧ A[n])⌝⋅) }

1
.....assertion..... 
1. [A] : ℕ ⟶ ℙ
2. ∀s:StrictInc. ∃n:ℕ. A[s n]
⊢ ∀m:ℕ. ∃n:ℕ. (m < n ∧ A[n])

2
1. [A] : ℕ ⟶ ℙ
2. ∀s:StrictInc. ∃n:ℕ. A[s n]
3. ∀m:ℕ. ∃n:ℕ. (m < n ∧ A[n])
⊢ ∃s:StrictInc. ∀n:ℕ. A[s n]

---

Latex:

---

Latex:
\mforall{}[A:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}s:StrictInc.  \mexists{}n:\mBbbN{}.  A[s  n])  {}\mRightarrow{}  (\mexists{}s:StrictInc.  \mforall{}n:\mBbbN{}.  A[s  n]))


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}\mforall{}m:\mBbbN{}.  \mexists{}n:\mBbbN{}.  (m  <  n  \mwedge{}  A[n])\mkleeneclose{}\mcdot{})

---

Home Index