lineMap_lt_map_iff_slope_lt_slope_right

English

Given c = lineMap(a, b, r) with 0 < (1 − r)(b − a), we have f(c) ≤ lineMap(f(a), f(b), r) iff slope f a b ≤ slope f a c.

Русский

Пусть c = lineMap(a, b, r) и 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),\ 0 < (1-r)(b-a) \Longrightarrow \\ f(c) \le \mathrm{lineMap}(f(a),f(b),r) \iff \operatorname{slope} f(a,b) \le \operatorname{slope} f(a,c).$$$

Lean4

/-- Given `c = lineMap a b r`, `c < b`, the point `(c, f c)` is strictly above the
segment `[(a, f a), (b, f b)]` if and only if `slope f c b < slope f a b`. -/
theorem lineMap_lt_map_iff_slope_lt_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_lt_lineMap_iff_slope_lt_slope_right (E := Eᵒᵈ) (f := f) (a := a) (b := b) (r := r) h

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