---

Step * 1 of Lemma u-almost-full-filter


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])
BY
{ (Unfold `u-almost-full` 0 THEN InstLemma `intuitionistic-pigeonhole` [⌜A⌝;⌜B⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}@i'
2.  B  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}@i'
3.  u-almost-full(n.A[n])@i
4.  u-almost-full(n.B[n])@i
\mvdash{}  u-almost-full(n.A[n]  \mwedge{}  B[n])


By

---

Latex:
(Unfold  `u-almost-full`  0  THEN  InstLemma  `intuitionistic-pigeonhole`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index