---

Step * 1 2 of Lemma nat-overt


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
BY
{ TACTIC:(InstLemma `sp-lub-property` [⌜λ2n.A <n, y>⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  Y  :  Type
2.  A  :  Open(\mBbbN{}  \mtimes{}  Y)@i
3.  B  :  Open(Y)@i
4.  \mforall{}x:\mBbbN{}.  \mforall{}y:Y.    A  <x,  y>  \mleq{}  B  y
5.  y  :  Y@i
\mvdash{}  lub(n.A  <n,  y>)  \mleq{}  B  y


By

---

Latex:
TACTIC:(InstLemma  `sp-lub-property`  [\mkleeneopen{}\mlambda{}\msubtwo{}n.A  <n,  y>\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index