---

Step * of Lemma general-fan-theorem-troelstra-sq

∀X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ. ((∀f:ℕ ⟶ 𝔹. ⇃(∃n:ℕ. X[n;f])) ⇒ ⇃(∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f]))
BY
{ (UnivCD THENA Auto) }

1
1. X : n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ@i'
2. ∀f:ℕ ⟶ 𝔹. ⇃(∃n:ℕ. X[n;f])@i
⊢ ⇃(∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f])

---

Latex:

---

Latex:
\mforall{}X:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \00D9(\mexists{}n:\mBbbN{}.  X[n;f]))  {}\mRightarrow{}  \00D9(\mexists{}k:\mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}n:\mBbbN{}k.  X[n;f]))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index