English
If a < c < b and 0 < (1 − r)(b − a) then f(c) ≤ lineMap(f(a), f(b), r) iff slope f a c ≤ slope f a b.
Русский
Если a < c < b и 0 < (1 − r)(b − a), то f(c) ≤ lineMap(f(a), f(b), r) тогда и только если slope f a c ≤ slope f a b.
LaTeX
$$$a < c < b \land 0 < (1-r)(b-a) \Longrightarrow \ f(c) \le \mathrm{lineMap}(f(a),f(b),r) \iff \operatorname{slope} f(a,c) \le \operatorname{slope} f(a,b).$$$
Lean4
/-- Given `c = lineMap a b r`, `a < c < b`, 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 c b`. -/
theorem map_lt_lineMap_iff_slope_lt_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 :=
lt_iff_lt_of_le_iff_le' (lineMap_le_map_iff_slope_le_slope hab h₀ h₁) (map_le_lineMap_iff_slope_le_slope hab h₀ h₁)
