English
For c = lineMap(a, b, r) with c < b, the inequality f((lineMap a b) r) ≤ lineMap(f(a), f(b), r) is equivalent to slope f a b ≤ slope f(lineMap a b r) b.
Русский
Пусть c = lineMap(a, b, r) и c < b. Тогда неравенство f( lineMap a b r ) ≤ lineMap(f(a), f(b), r) эквивалентно slope f a b ≤ slope f( lineMap a b r ) b.
LaTeX
$$$c = \mathrm{lineMap}(a,b,r),\ c < b \Longrightarrow \\ f((\mathrm{lineMap}(a,b))(r)) \le \mathrm{lineMap}(f(a),f(b),r) \iff \operatorname{slope} f(a,b) \le \operatorname{slope} f(\mathrm{lineMap}(a,b), b).$$$
Lean4
/-- Given `c = lineMap a b r`, `a < c < b`, the point `(c, f c)` is non-strictly below the
segment `[(a, f a), (b, f b)]` if and only if `slope f a c ≤ slope f c b`. -/
theorem map_le_lineMap_iff_slope_le_slope (hab : a < b) (h₀ : 0 < r) (h₁ : r < 1) :
f c ≤ lineMap (f a) (f b) r ↔ slope f a c ≤ slope f c b := by
rw [map_le_lineMap_iff_slope_le_slope_left (mul_pos h₀ (sub_pos.2 hab)), ←
lineMap_slope_lineMap_slope_lineMap f a b r, right_le_lineMap_iff_le h₁]
