midpoint_le_midpoint — Mathlib

English

If a ≤ a' and b ≤ b', then midpoint k a b ≤ midpoint k a' b'.

Русский

Если a ≤ a' и b ≤ b', то середина между a и b не превосходит середину между a' и b'.

LaTeX

$$$a \le a' \wedge b \le b' \rightarrow \operatorname{midpoint}(k,a,b) \le \operatorname{midpoint}(k,a',b')$$$

Lean4

theorem midpoint_le_midpoint [Invertible (2 : k)] (ha : a ≤ a') (hb : b ≤ b') : midpoint k a b ≤ midpoint k a' b' :=
  lineMap_mono_endpoints ha hb (invOf_nonneg.2 zero_le_two) <| invOf_le_one one_le_two

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