---

Step * 1 of Lemma nat-overt


1. [Y] : Type
⊢ ∃ex:Open(ℕ × Y) ⟶ Open(Y). ∀A:Open(ℕ × Y). ∀B:Open(Y).  (∀y:Y. ex A y ≤ B y ⇐⇒ ∀x:ℕ. ∀y:Y.  A <x, y> ≤ B y)
BY
{ TACTIC:(InstConcl [⌜λA,y. lub(n.A <n, y>)⌝]⋅ THEN Reduce 0 THEN Auto) }

1
1. Y : Type
2. A : Open(ℕ × Y)@i
3. B : Open(Y)@i
4. ∀y:Y. lub(n.A <n, y>) ≤ B y
5. x : ℕ@i
6. y : Y@i
⊢ A <x, y> ≤ B y

2
1. Y : Type
2. A : Open(ℕ × Y)@i
3. B : Open(Y)@i
4. ∀x:ℕ. ∀y:Y.  A <x, y> ≤ B y
5. y : Y@i
⊢ lub(n.A <n, y>) ≤ B y

---

Latex:

---

Latex:

1.  [Y]  :  Type
\mvdash{}  \mexists{}ex:Open(\mBbbN{}  \mtimes{}  Y)  {}\mrightarrow{}  Open(Y)
      \mforall{}A:Open(\mBbbN{}  \mtimes{}  Y).  \mforall{}B:Open(Y).    (\mforall{}y:Y.  ex  A  y  \mleq{}  B  y  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x:\mBbbN{}.  \mforall{}y:Y.    A  <x,  y>  \mleq{}  B  y)


By

---

Latex:
TACTIC:(InstConcl  [\mkleeneopen{}\mlambda{}A,y.  lub(n.A  <n,  y>)\mkleeneclose{}]\mcdot{}  THEN  Reduce  0  THEN  Auto)

---

Home Index