---

Step * 1 of Lemma u-almost-full-finite-intersection


1. A : ℕ0 ⟶ ℕ ⟶ ℙ
2. ∀i:ℕ0. u-almost-full(n.A[i;n])
⊢ u-almost-full(n.∀i:ℕ0. A[i;n])
BY
{ (InstLemma `u-almost-full-filter` [⌜λ2n.True⌝;⌜⌜λ2n.∀i:ℕ0. A[i;n]⌝⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  \mBbbN{}0  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  \mforall{}i:\mBbbN{}0.  u-almost-full(n.A[i;n])
\mvdash{}  u-almost-full(n.\mforall{}i:\mBbbN{}0.  A[i;n])


By

---

Latex:
(InstLemma  `u-almost-full-filter`  [\mkleeneopen{}\mlambda{}\msubtwo{}n.True\mkleeneclose{};\mkleeneopen{}\mkleeneopen{}\mlambda{}\msubtwo{}n.\mforall{}i:\mBbbN{}0.  A[i;n]\mkleeneclose{}\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index