---

Step * of Lemma interval-fun-real-fun

No Annotations
∀[a,b:ℝ]. ∀[f:[a, b] ⟶ℝ].  real-fun(f;a;b) supposing ∃J:Interval. interval-fun([a, b];J;x.f[x])
BY
{ (Auto THEN ExRepD THEN D -1 THEN Unfold `real-fun` 0 THEN RepeatFor 3 (ParallelLast)) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[a,b:\mBbbR{}].  \mforall{}[f:[a,  b]  {}\mrightarrow{}\mBbbR{}].    real-fun(f;a;b)  supposing  \mexists{}J:Interval.  interval-fun([a,  b];J;x.f[x])


By

---

Latex:
(Auto  THEN  ExRepD  THEN  D  -1  THEN  Unfold  `real-fun`  0  THEN  RepeatFor  3  (ParallelLast))

---

Home Index