---

Step * of Lemma nat-inf-limit

No Annotations
∀p:ℕ∞ ⟶ 𝔹. ((∀n:ℕ. p n∞ = ff) ⇒ p ∞ = ff)
BY
{ (Auto THEN BoolCase ⌜p ∞⌝⋅ THEN Auto THEN InstLemma `no-weak-limited-omniscience` [] THEN D -1) }

1
1. p : ℕ∞ ⟶ 𝔹
2. ∀n:ℕ. p n∞ = ff
3. ↑(p ∞)
⊢ ∀f:ℕ ⟶ 𝔹. Dec(∀n:ℕ. f n = ff)

---

Latex:

---

Latex:
No  Annotations
\mforall{}p:\mBbbN{}\minfty{}  {}\mrightarrow{}  \mBbbB{}.  ((\mforall{}n:\mBbbN{}.  p  n\minfty{}  =  ff)  {}\mRightarrow{}  p  \minfty{}  =  ff)


By

---

Latex:
(Auto  THEN  BoolCase  \mkleeneopen{}p  \minfty{}\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  InstLemma  `no-weak-limited-omniscience`  []  THEN  D  -1)

---

Home Index