---

Step * of Lemma interior-dense-in-interval

∀a,b:ℝ.  dense-in-interval([a, b];λr.((a < r) ∧ (r < b)))
BY
{ (Auto THEN D 0 THEN Reduce 0 THEN Auto) }

1
1. a : ℝ
2. b : ℝ
3. a@0 : {a@0:ℝ| a@0 ∈ [a, b]} 
4. b@0 : {r:ℝ| (a ≤ r) ∧ (r ≤ b)} 
5. a@0 < b@0
⊢ ∃x:ℝ. (((a < x) ∧ (x < b)) ∧ (a@0 < x) ∧ (x < b@0))

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.    dense-in-interval([a,  b];\mlambda{}r.((a  <  r)  \mwedge{}  (r  <  b)))


By

---

Latex:
(Auto  THEN  D  0  THEN  Reduce  0  THEN  Auto)

---

Home Index