---

Step * of Lemma not-discontinuous

∀[f:ℝ ⟶ ℝ]. ∀[x:ℝ]. (¬discontinuous(f;x)) supposing ∀x,y:ℝ.  ((x = y) ⇒ ((f x) = (f y)))
BY
{ (Auto THEN (D 0 THENA Auto)) }

1
1. f : ℝ ⟶ ℝ
2. ∀x,y:ℝ.  ((x = y) ⇒ ((f x) = (f y)))
3. x : ℝ
4. discontinuous(f;x)
⊢ False

---

Latex:

---

Latex:
\mforall{}[f:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[x:\mBbbR{}].  (\mneg{}discontinuous(f;x))  supposing  \mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  ((f  x)  =  (f  y)))


By

---

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

---

Home Index