---

Step * 1 of Lemma compact-dCCC


1. K : Type
2. k : K
3. compact-type(K)
4. R : ℕ ⟶ K ⟶ 𝔹
5. ∀g:ℕ ⟶ K. ∃n:ℕ. (↑(R n (g n)))
6. d : ∀n:ℕ. ((∃m:K. (¬↑(R n m))) ∨ (∀m:K. (↑(R n m))))
⊢ ∃n:ℕ. ∀m:K. (↑(R n m))
BY
{ ((D -2 With ⌜λn.case d n of inl(p) => fst(p) | inr(_) => k⌝  THENA Auto) THEN Reduce -1) }

1
1. K : Type
2. k : K
3. compact-type(K)
4. R : ℕ ⟶ K ⟶ 𝔹
5. d : ∀n:ℕ. ((∃m:K. (¬↑(R n m))) ∨ (∀m:K. (↑(R n m))))
6. ∃n:ℕ. (↑(R n case d n of inl(p) => fst(p) | inr(_) => k))
⊢ ∃n:ℕ. ∀m:K. (↑(R n m))

---

Latex:

---

Latex:

1.  K  :  Type
2.  k  :  K
3.  compact-type(K)
4.  R  :  \mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbB{}
5.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  K.  \mexists{}n:\mBbbN{}.  (\muparrow{}(R  n  (g  n)))
6.  d  :  \mforall{}n:\mBbbN{}.  ((\mexists{}m:K.  (\mneg{}\muparrow{}(R  n  m)))  \mvee{}  (\mforall{}m:K.  (\muparrow{}(R  n  m))))
\mvdash{}  \mexists{}n:\mBbbN{}.  \mforall{}m:K.  (\muparrow{}(R  n  m))


By

---

Latex:
((D  -2  With  \mkleeneopen{}\mlambda{}n.case  d  n  of  inl(p)  =>  fst(p)  |  inr($_{}$)  =>  k\mkleeneclose{}    THENA  Auto)  THE\000CN  Reduce  -1)

---

Home Index