English
Let c = lineMap(a, b, r) with a < c and 0 < r(b − a). Then the point (c, f(c)) is strictly below the segment [(a, f(a)), (b, f(b))] if and only if slope f(a, c) < slope f(a, b).
Русский
Пусть c = lineMap(a, b, r) и a < c, 0 < r(b − a). Тогда точка (c, f(c)) строго ниже сегмента [(a, f(a)), (b, f(b))] тогда и только тогда, когда наклон между a и c меньше наклона между a и b.
LaTeX
$$$c = \mathrm{lineMap}(a,b,r),\ a < c,\ 0 < r(b-a) \Longrightarrow \\ f(c) < \mathrm{lineMap}(f(a), f(b), r) \iff \operatorname{slope} f(a,c) < \operatorname{slope} f(a,b).$$$
Lean4
/-- Given `c = lineMap a b r`, `a < c`, the point `(c, f c)` is strictly below the
segment `[(a, f a), (b, f b)]` if and only if `slope f a c < slope f a b`. -/
theorem map_lt_lineMap_iff_slope_lt_slope_left (h : 0 < r * (b - a)) :
f c < lineMap (f a) (f b) r ↔ slope f a c < slope f a b :=
lt_iff_lt_of_le_iff_le' (lineMap_le_map_iff_slope_le_slope_left h) (map_le_lineMap_iff_slope_le_slope_left h)
