---

Step * of Lemma strict-increasing-implies-inv-strict-increasing

∀[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)))) and 
     (∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ ((f x) = (f y)))))
BY
{ (InstLemma `real-fun-implies-sfun-general` [] THEN RepeatFor 3 (ParallelLast') THEN Auto THEN (Unhide THENA Auto)) }

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

---

Latex:

---

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


By

---

Latex:
(InstLemma  `real-fun-implies-sfun-general`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  Auto
  THEN  (Unhide  THENA  Auto))

---

Home Index