lineMap_le_map_iff_slope_le_slope_right

English

Let c = lineMap(a, b, r) with a < c < b. Then f(c) < lineMap(f(a), f(b), r) iff slope f(a, b) < slope f(c, b).

Русский

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

LaTeX

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

Lean4

/-- Given `c = lineMap a b r`, `c < b`, the point `(c, f c)` is non-strictly above the
segment `[(a, f a), (b, f b)]` if and only if `slope f c b ≤ slope f a b`. -/
theorem lineMap_le_map_iff_slope_le_slope_right (h : 0 < (1 - r) * (b - a)) :
    lineMap (f a) (f b) r ≤ f c ↔ slope f c b ≤ slope f a b :=
  map_le_lineMap_iff_slope_le_slope_right (E := Eᵒᵈ) (f := f) (a := a) (b := b) (r := r) h

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