English
For a < b and 0 < r < 1, with c = lineMap(a,b,r) and a < c < b, the statement f(c) ≤ lineMap(f(a), f(b), r) is equivalent to slope f a c ≤ slope f c b.
Русский
Для a < b и 0 < r < 1, пусть c = lineMap(a,b,r) и a < c < b. Тогда f(c) ≤ lineMap(f(a), f(b), r) эквивалентно slope f a c ≤ slope f c b.
LaTeX
$$$a < b,\ 0 < r < 1,\ c = \mathrm{lineMap}(a,b,r) \Rightarrow f(c) \le \mathrm{lineMap}(f(a),f(b),r) \iff \operatorname{slope} f(a,c) \le \operatorname{slope} f(c,b).$$$
Lean4
/-- Given `c = lineMap a b r`, `a < c < b`, the point `(c, f c)` is strictly above the
segment `[(a, f a), (b, f b)]` if and only if `slope f c b < slope f a c`. -/
theorem lineMap_lt_map_iff_slope_lt_slope (hab : a < b) (h₀ : 0 < r) (h₁ : r < 1) :
lineMap (f a) (f b) r < f c ↔ slope f c b < slope f a c :=
map_lt_lineMap_iff_slope_lt_slope (E := Eᵒᵈ) hab h₀ h₁
