---

Step * 1 of Lemma sp-lub-property


1. A : ℕ ⟶ Sierpinski
2. n : ℕ@i
⊢ A[n] ≤ lub(n.A[n])
BY
{ TACTIC:(D 0 THEN Auto THEN BLemma `sp-lub-is-top` THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  \mBbbN{}  {}\mrightarrow{}  Sierpinski
2.  n  :  \mBbbN{}@i
\mvdash{}  A[n]  \mleq{}  lub(n.A[n])


By

---

Latex:
TACTIC:(D  0  THEN  Auto  THEN  BLemma  `sp-lub-is-top`  THEN  Auto)

---

Home Index