---

Step * of Lemma no-weak-limited-omniscience

¬(∀f:ℕ ⟶ 𝔹. Dec(∀n:ℕ. f n = ff))
BY
{ ((Assert weak-continuity(𝔹;𝔹) BY Auto) THEN (D 0 THENA Auto)) }

1
1. weak-continuity(𝔹;𝔹)
2. ∀f:ℕ ⟶ 𝔹. Dec(∀n:ℕ. f n = ff)
⊢ False

---

Latex:

---

Latex:
\mneg{}(\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  Dec(\mforall{}n:\mBbbN{}.  f  n  =  ff))


By

---

Latex:
((Assert  weak-continuity(\mBbbB{};\mBbbB{})  BY  Auto)  THEN  (D  0  THENA  Auto))

---

Home Index