---

Step * of Lemma interval-retraction-req

∀[u,v:ℝ]. ∀[x:{x:ℝ| x ∈ [u, v]} ].  (interval-retraction(u;v;x) = x)
BY
{ (Intros
   THEN (Assert x ∈ [u, v] BY
               (Reduce 0 THEN Unhide THEN Auto))
   THEN Reduce -1
   THEN (Assert u ≤ v BY
               Auto)
   THEN Unfold `interval-retraction` 0) }

1
1. [u] : ℝ
2. [v] : ℝ
3. [x] : {x:ℝ| x ∈ [u, v]} 
4. (u ≤ x) ∧ (x ≤ v)
5. u ≤ v
⊢ rmin(v;rmax(u;x)) = x

---

Latex:

---

Latex:
\mforall{}[u,v:\mBbbR{}].  \mforall{}[x:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}  ].    (interval-retraction(u;v;x)  =  x)


By

---

Latex:
(Intros
  THEN  (Assert  x  \mmember{}  [u,  v]  BY
                          (Reduce  0  THEN  Unhide  THEN  Auto))
  THEN  Reduce  -1
  THEN  (Assert  u  \mleq{}  v  BY
                          Auto)
  THEN  Unfold  `interval-retraction`  0)

---

Home Index