English
The midpoint respects linear order and is compatible with endpoints in inequalities.
Русский
Середина сохраняет линейный порядок и совместима с концами в неравенствах.
LaTeX
$$$a \le a' \rightarrow (\operatorname{midpoint}(k,a,b) \le \operatorname{midpoint}(k,a',b') \text{ при } b \le b')$$$
Lean4
/-- Given `c = lineMap a b r`, `a < c`, the point `(c, f c)` is non-strictly below the
segment `[(a, f a), (b, f b)]` if and only if `slope f a c ≤ slope f a b`. -/
theorem map_le_lineMap_iff_slope_le_slope_left (h : 0 < r * (b - a)) :
f c ≤ lineMap (f a) (f b) r ↔ slope f a c ≤ slope f a b := by
rw [lineMap_apply, lineMap_apply, slope, slope, vsub_eq_sub, vsub_eq_sub, vsub_eq_sub, vadd_eq_add, vadd_eq_add,
smul_eq_mul, add_sub_cancel_right, smul_sub, smul_sub, smul_sub, sub_le_iff_le_add, mul_inv_rev, mul_smul, mul_smul,
← smul_sub, ← smul_sub, ← smul_add, smul_smul, ← mul_inv_rev, inv_smul_le_iff_of_pos h, smul_smul,
mul_inv_cancel_right₀ (right_ne_zero_of_mul h.ne'), smul_add, smul_inv_smul₀ (left_ne_zero_of_mul h.ne')]
