---

Step * 1 1 1 1 of Lemma nat-overt


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
7. lub(n.A <n, y>) ≤ B y
8. ∀n:ℕ. A <n, y> ≤ lub(n.A <n, y>)
9. ∀c:Sierpinski. ((∀n:ℕ. A <n, y> ≤ c) ⇒ lub(n.A <n, y>) ≤ c)
⊢ A <x, y> ≤ B y
BY
{ TACTIC:(InstHyp [⌜x⌝] (-2)⋅ THENA 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
7. lub(n.A <n, y>) ≤ B y
8. ∀n:ℕ. A <n, y> ≤ lub(n.A <n, y>)
9. ∀c:Sierpinski. ((∀n:ℕ. A <n, y> ≤ c) ⇒ lub(n.A <n, y>) ≤ c)
10. A <x, y> ≤ lub(n.A <n, y>)
⊢ A <x, y> ≤ B y

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:(InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)

---

Home Index