map_le_lineMap_iff_slope_le_slope_right

English

For c = lineMap(a, b, r) with a < 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.

Русский

Пусть c = lineMap(a, b, r) и a < c < b. Тогда точка (c, f(c)) строго выше сегмента [(a, f(a)), (b, f(b))] тогда и только если наклон между c и b меньше или равен наклону между a и 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 below the
segment `[(a, f a), (b, f b)]` if and only if `slope f a b ≤ slope f c b`. -/
theorem map_le_lineMap_iff_slope_le_slope_right (h : 0 < (1 - r) * (b - a)) :
    f c ≤ lineMap (f a) (f b) r ↔ slope f a b ≤ slope f c b :=
  by
  rw [← lineMap_apply_one_sub, ← lineMap_apply_one_sub _ _ r]
  revert h; generalize 1 - r = r'; clear! r; intro h
  simp_rw [lineMap_apply, slope, vsub_eq_sub, vadd_eq_add, smul_eq_mul]
  rw [sub_add_eq_sub_sub_swap, sub_self, zero_sub, neg_mul_eq_mul_neg, neg_sub, le_inv_smul_iff_of_pos h, smul_smul,
    mul_inv_cancel_right₀, le_sub_comm, ← neg_sub (f b), smul_neg, neg_add_eq_sub]
  · exact right_ne_zero_of_mul h.ne'

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