---

Step * of Lemma unsquashed-weak-continuity-false

¬unsquashed-WCP
BY
{ (InstLemma `Escardo-Xu` [] THEN ParallelLast) }

1
1. unsquashed-WCP
⊢ ∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∃k:ℕ. ∀g:ℕ ⟶ ℕ. ((∀i:ℕk. ((g i) = 0 ∈ ℕ)) ⇒ ((F (λi.0)) = (F g) ∈ ℕ))

---

Latex:

---

Latex:
\mneg{}unsquashed-WCP


By

---

Latex:
(InstLemma  `Escardo-Xu`  []  THEN  ParallelLast)

---

Home Index