---

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


1. X : n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ@i'
2. ∀f:ℕ ⟶ 𝔹. ⇃(∃n:ℕ. X[n;f])@i
3. ⇃(∃F:(ℕ ⟶ 𝔹) ⟶ ℕ. ∀f:ℕ ⟶ 𝔹. (X (F f) f))
⊢ ⇃(∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f])
BY
{ ((BLemma `prop-truncation-quot` THENA Auto)
   THEN MoveToConcl (-1)
   THEN (BLemma `implies-quotient-true` THEN Auto)
   THEN (BLemma `general-fan-theorem-troelstra` THENA Auto)) }

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

---

Latex:

---

Latex:

1.  X  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbP{}@i'
2.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \00D9(\mexists{}n:\mBbbN{}.  X[n;f])@i
3.  \00D9(\mexists{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  (X  (F  f)  f))
\mvdash{}  \00D9(\mexists{}k:\mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}n:\mBbbN{}k.  X[n;f])


By

---

Latex:
((BLemma  `prop-truncation-quot`  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (BLemma  `implies-quotient-true`  THEN  Auto)
  THEN  (BLemma  `general-fan-theorem-troelstra`  THENA  Auto))

---

Home Index