---

Step * 1 of Lemma interior-dense-in-interval


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))
BY
{ (RenameVar `u' (-3)
   THEN RenameVar `v' (-2)
   THEN (InstLemma `ravg-between` [⌜u⌝;⌜v⌝]⋅ THENA Auto)
   THEN D 0 With ⌜ravg(u;v)⌝ 
   THEN Auto
   THEN All Reduce
   THEN DSetVars
   THEN Unhide
   THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  a@0  :  \{a@0:\mBbbR{}|  a@0  \mmember{}  [a,  b]\} 
4.  b@0  :  \{r:\mBbbR{}|  (a  \mleq{}  r)  \mwedge{}  (r  \mleq{}  b)\} 
5.  a@0  <  b@0
\mvdash{}  \mexists{}x:\mBbbR{}.  (((a  <  x)  \mwedge{}  (x  <  b))  \mwedge{}  (a@0  <  x)  \mwedge{}  (x  <  b@0))


By

---

Latex:
(RenameVar  `u'  (-3)
  THEN  RenameVar  `v'  (-2)
  THEN  (InstLemma  `ravg-between`  [\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  0  With  \mkleeneopen{}ravg(u;v)\mkleeneclose{} 
  THEN  Auto
  THEN  All  Reduce
  THEN  DSetVars
  THEN  Unhide
  THEN  Auto)

---

Home Index