---

Step * of Lemma sup-iff-closure

No Annotations
∀[A:Set(ℝ)]. ∀x:ℝ. (sup(A) = x ⇐⇒ A ≤ x ∧ x ∈ closure(A))
BY
{ (Unfolds ``sup member-closure`` 0 THEN Auto) }

1
1. [A] : Set(ℝ)
2. x : ℝ
3. A ≤ x
4. ∀e:ℝ. ((r0 < e) ⇒ (∃x@0:ℝ. ((x@0 ∈ A) ∧ ((x - e) < x@0))))
⊢ ∃x@0:ℕ ⟶ ℝ. (lim n→∞.x@0[n] = x ∧ (∀n:ℕ. (A x@0[n])))

2
1. [A] : Set(ℝ)
2. x : ℝ
3. A ≤ x
4. ∃x@0:ℕ ⟶ ℝ. (lim n→∞.x@0[n] = x ∧ (∀n:ℕ. (A x@0[n])))
5. e : ℝ
6. r0 < e
⊢ ∃x@0:ℝ. ((x@0 ∈ A) ∧ ((x - e) < x@0))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A:Set(\mBbbR{})].  \mforall{}x:\mBbbR{}.  (sup(A)  =  x  \mLeftarrow{}{}\mRightarrow{}  A  \mleq{}  x  \mwedge{}  x  \mmember{}  closure(A))


By

---

Latex:
(Unfolds  ``sup  member-closure``  0  THEN  Auto)

---

Home Index