---

Step * of Lemma nat-strong-overt-implies-Markov

sOvert(ℕ) ⇒ (∀g:ℕ ⟶ 𝔹. ((¬(∀n:ℕ. g n = ff)) ⇒ (∃n:ℕ. g n = tt)))
BY
{ (Auto THEN (With ⌜Unit⌝ (D 1)⋅ THENA Auto) THEN ExRepD THEN All (RepUR ``Open in-open``)) }

1
1. g : ℕ ⟶ 𝔹@i
2. ¬(∀n:ℕ. g n = ff)
3. f : ((ℕ × Unit) ⟶ Sierpinski) ⟶ Unit ⟶ Sierpinski@i'
4. ∀A:(ℕ × Unit) ⟶ Sierpinski. ∀y:Unit.  ((f A y) = ⊤ ∈ Sierpinski ⇐⇒ ∃x:ℕ. ((A <x, y>) = ⊤ ∈ Sierpinski))
⊢ ∃n:ℕ. g n = tt

---

Latex:

---

Latex:
sOvert(\mBbbN{})  {}\mRightarrow{}  (\mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  ((\mneg{}(\mforall{}n:\mBbbN{}.  g  n  =  ff))  {}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  g  n  =  tt)))


By

---

Latex:
(Auto  THEN  (With  \mkleeneopen{}Unit\mkleeneclose{}  (D  1)\mcdot{}  THENA  Auto)  THEN  ExRepD  THEN  All  (RepUR  ``Open  in-open``))

---

Home Index