---

Step * 1 2 of Lemma nat-weak-overt


1. [Y] : Type
⊢ ∀A:Open(ℕ × Y). ∀y:Y.  (y ∈ (λA,y. lub(n.A <n, y>)) A ⇐⇒ ¬¬(∃x:ℕ. <x, y> ∈ A))
BY
{ TACTIC:(RepUR ``in-open`` 0 THEN (UnivCD THENA Auto)) }

1
1. Y : Type
2. A : Open(ℕ × Y)@i
3. y : Y@i
⊢ lub(n.A <n, y>) = ⊤ ∈ Sierpinski ⇐⇒ ¬¬(∃x:ℕ. ((A <x, y>) = ⊤ ∈ Sierpinski))

---

Latex:

---

Latex:

1.  [Y]  :  Type
\mvdash{}  \mforall{}A:Open(\mBbbN{}  \mtimes{}  Y).  \mforall{}y:Y.    (y  \mmember{}  (\mlambda{}A,y.  lub(n.A  <n,  y>))  A  \mLeftarrow{}{}\mRightarrow{}  \mneg{}\mneg{}(\mexists{}x:\mBbbN{}.  <x,  y>  \mmember{}  A))


By

---

Latex:
TACTIC:(RepUR  ``in-open``  0  THEN  (UnivCD  THENA  Auto))

---

Home Index