---

Step * of Lemma rleq_inf

∀[A:Set(ℝ)]. ∀[b,c:ℝ].  (inf(A) = b ⇒ (c ≤ b ⇐⇒ ∀x:ℝ. ((x ∈ A) ⇒ (c ≤ x))))
BY
{ (Auto THEN D 4) }

1
1. A : Set(ℝ)
2. b : ℝ
3. c : ℝ
4. lower-bound(A;b)
5. ∀e:ℝ. ((r0 < e) ⇒ (∃x:ℝ. ((x ∈ A) ∧ (x < (b + e)))))
6. c ≤ b
7. x : ℝ
8. x ∈ A
⊢ c ≤ x

2
1. A : Set(ℝ)
2. b : ℝ
3. c : ℝ
4. lower-bound(A;b)
5. ∀e:ℝ. ((r0 < e) ⇒ (∃x:ℝ. ((x ∈ A) ∧ (x < (b + e)))))
6. ∀x:ℝ. ((x ∈ A) ⇒ (c ≤ x))
⊢ c ≤ b

---

Latex:

---

Latex:
\mforall{}[A:Set(\mBbbR{})].  \mforall{}[b,c:\mBbbR{}].    (inf(A)  =  b  {}\mRightarrow{}  (c  \mleq{}  b  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  A)  {}\mRightarrow{}  (c  \mleq{}  x))))


By

---

Latex:
(Auto  THEN  D  4)

---

Home Index