---

Step * of Lemma old-proof-of-real-continuity

No Annotations
∀a,b:ℝ.  ∀f:[a, b] ⟶ℝ. real-cont(f;a;b) supposing real-fun(f;a;b) supposing a ≤ b
BY
{ (Auto THEN (FLemma `real-fun-implies-sfun` [-1] THENA Auto)) }

1
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. f : [a, b] ⟶ℝ
5. real-fun(f;a;b)
6. real-sfun(f;a;b)
⊢ real-cont(f;a;b)

---

Latex:

---

Latex:
No  Annotations
\mforall{}a,b:\mBbbR{}.    \mforall{}f:[a,  b]  {}\mrightarrow{}\mBbbR{}.  real-cont(f;a;b)  supposing  real-fun(f;a;b)  supposing  a  \mleq{}  b


By

---

Latex:
(Auto  THEN  (FLemma  `real-fun-implies-sfun`  [-1]  THENA  Auto))

---

Home Index