---

Step * of Lemma u-almost-full-filter

∀A,B:ℕ ⟶ ℙ.
  ((u-almost-full(n.A[n]) ⇒ u-almost-full(n.B[n]) ⇒ u-almost-full(n.A[n] ∧ B[n]))
  ∧ ((∀n:ℕ. (A[n] ⇒ B[n])) ⇒ u-almost-full(n.A[n]) ⇒ u-almost-full(n.B[n]))
  ∧ u-almost-full(n.True))
BY
{ Auto }

1
1. A : ℕ ⟶ ℙ@i'
2. B : ℕ ⟶ ℙ@i'
3. u-almost-full(n.A[n])@i
4. u-almost-full(n.B[n])@i
⊢ u-almost-full(n.A[n] ∧ B[n])

2
1. A : ℕ ⟶ ℙ@i'
2. B : ℕ ⟶ ℙ@i'
3. ∀n:ℕ. (A[n] ⇒ B[n])@i
4. u-almost-full(n.A[n])@i
5. u-almost-full(n.B[n]) ⇒ u-almost-full(n.A[n] ∧ B[n])
⊢ u-almost-full(n.B[n])

3
1. A : ℕ ⟶ ℙ@i'
2. B : ℕ ⟶ ℙ@i'
3. u-almost-full(n.A[n]) ⇒ u-almost-full(n.B[n]) ⇒ u-almost-full(n.A[n] ∧ B[n])
4. (∀n:ℕ. (A[n] ⇒ B[n])) ⇒ u-almost-full(n.A[n]) ⇒ u-almost-full(n.B[n])
⊢ u-almost-full(n.True)

---

Latex:

---

Latex:
\mforall{}A,B:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}.
    ((u-almost-full(n.A[n])  {}\mRightarrow{}  u-almost-full(n.B[n])  {}\mRightarrow{}  u-almost-full(n.A[n]  \mwedge{}  B[n]))
    \mwedge{}  ((\mforall{}n:\mBbbN{}.  (A[n]  {}\mRightarrow{}  B[n]))  {}\mRightarrow{}  u-almost-full(n.A[n])  {}\mRightarrow{}  u-almost-full(n.B[n]))
    \mwedge{}  u-almost-full(n.True))


By

---

Latex:
Auto

---

Home Index