---

Step * of Lemma intuitionistic-pigeonhole1

∀[A,B:ℕ ⟶ ℙ].
  ((∀s:StrictInc. ∃n:ℕ. A[s n]) ⇒ (∀s:StrictInc. ∃n:ℕ. B[s n]) ⇒ (∀s:StrictInc. ∃n:ℕ. (A[s n] ∧ B[s n])))
BY
{ (Auto THEN (InstLemma `unary-strong-almost-full-has-strict-inc` [⌜λ2n.A[s n]⌝]⋅ THENA Auto)) }

1
1. [A] : ℕ ⟶ ℙ
2. [B] : ℕ ⟶ ℙ
3. ∀s:StrictInc. ∃n:ℕ. A[s n]@i
4. ∀s:StrictInc. ∃n:ℕ. B[s n]@i
5. s : StrictInc@i
6. s@0 : StrictInc@i
⊢ ∃n:ℕ. A[s (s@0 n)]

2
1. [A] : ℕ ⟶ ℙ
2. [B] : ℕ ⟶ ℙ
3. ∀s:StrictInc. ∃n:ℕ. A[s n]@i
4. ∀s:StrictInc. ∃n:ℕ. B[s n]@i
5. s : StrictInc@i
6. ∃s@0:StrictInc. ∀n:ℕ. A[s (s@0 n)]
⊢ ∃n:ℕ. (A[s n] ∧ B[s n])

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (InstLemma  `unary-strong-almost-full-has-strict-inc`  [\mkleeneopen{}\mlambda{}\msubtwo{}n.A[s  n]\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index