map_lt_lineMap_iff_slope_lt_slope_right

English

If c = lineMap(a, b, r) with a < c and c < b and 0 < (1 − r)(b − a), then f(c) ≤ lineMap(f(a), f(b), r) iff slope f(a, b) ≤ slope f(a, c).

Русский

Пусть c = lineMap(a, b, r) с a < c < b и 0 < (1 − r)(b − a). Тогда f(c) ≤ lineMap(f(a), f(b), r) тогда и только если slope f(a, b) ≤ slope f(a, c).

LaTeX

$$$c = \mathrm{lineMap}(a,b,r),\ a

Lean4

/-- Given `c = lineMap a b r`, `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 b < slope f c b`. -/
theorem map_lt_lineMap_iff_slope_lt_slope_right (h : 0 < (1 - r) * (b - a)) :
    f c < lineMap (f a) (f b) r ↔ slope f a b < slope f c b :=
  lt_iff_lt_of_le_iff_le' (lineMap_le_map_iff_slope_le_slope_right h) (map_le_lineMap_iff_slope_le_slope_right h)

Похожие утверждения