---

Step * of Lemma real-fun-implies-sfun-general

∀[I:Interval]. ∀[f:I ⟶ℝ].
  ∀x,y:{x:ℝ| x ∈ I} .  (f x ≠ f y ⇒ x ≠ y) supposing ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ ((f x) = (f y)))
BY
{ (Auto THEN (BLemma `real-weak-Markov` THENA Auto)) }

1
1. I : Interval
2. f : I ⟶ℝ
3. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ ((f x) = (f y)))
4. x : {x:ℝ| x ∈ I} 
5. y : {x:ℝ| x ∈ I} 
6. f x ≠ f y
⊢ ∀z:ℝ. ((¬(z = x)) ∨ (¬(z = y)))

---

Latex:

---

Latex:
\mforall{}[I:Interval].  \mforall{}[f:I  {}\mrightarrow{}\mBbbR{}].
    \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    (f  x  \mneq{}  f  y  {}\mRightarrow{}  x  \mneq{}  y) 
    supposing  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  ((f  x)  =  (f  y)))


By

---

Latex:
(Auto  THEN  (BLemma  `real-weak-Markov`  THENA  Auto))

---

Home Index