---

Step * of Lemma r-strict-bound-property

∀x:ℝ. ((r(-(r-bound(x) + 1)) < x) ∧ (x < r(r-bound(x) + 1)))
BY
{ (InstLemma `r-bound-property` [] THEN ParallelLast THEN Auto) }

1
1. ∀[x:ℝ]. ((r(-r-bound(x)) ≤ x) ∧ (x ≤ r(r-bound(x))))
2. x : ℝ
3. r(-r-bound(x)) ≤ x
4. x ≤ r(r-bound(x))
⊢ r(-(r-bound(x) + 1)) < x

2
1. ∀[x:ℝ]. ((r(-r-bound(x)) ≤ x) ∧ (x ≤ r(r-bound(x))))
2. x : ℝ
3. r(-r-bound(x)) ≤ x
4. x ≤ r(r-bound(x))
5. r(-(r-bound(x) + 1)) < x
⊢ x < r(r-bound(x) + 1)

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  ((r(-(r-bound(x)  +  1))  <  x)  \mwedge{}  (x  <  r(r-bound(x)  +  1)))


By

---

Latex:
(InstLemma  `r-bound-property`  []  THEN  ParallelLast  THEN  Auto)

---

Home Index