lineMap_le_map_iff_slope_le_slope

English

Let c = lineMap(a,b,r) with a < b, 0 < r, and r < 1. Then f(c) ≤ lineMap(f(a), f(b), r) is equivalent to slope f a c ≤ slope f c b.

Русский

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

LaTeX

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

Lean4

/-- Given `c = lineMap a b r`, `a < 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 c`. -/
theorem lineMap_le_map_iff_slope_le_slope (hab : a < b) (h₀ : 0 < r) (h₁ : r < 1) :
    lineMap (f a) (f b) r ≤ f c ↔ slope f c b ≤ slope f a c :=
  map_le_lineMap_iff_slope_le_slope (E := Eᵒᵈ) hab h₀ h₁

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