lineMap_lt_map_iff_slope_lt_slope_left

English

Given c = lineMap(a, b, r) with a < c and 0 < (1 − r)(b − a), the point (f(a), f(b)) along the line at parameter r is below or equal to the endpoint f(c) iff slope f(a, b) ≤ slope f(c, b).

Русский

Пусть c = lineMap(a, b, r) и a < c, 0 < (1 − r)(b − a). Тогда точка на линии между f(a) и f(b) на параметре r лежит не выше точки f(c) тогда и только если наклон f между a и b меньше или равен наклону между c и b.

LaTeX

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

Lean4

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

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