dist_mono_right_pi — Mathlib

English

If a₂ ≤ a₁ ≤ b₁ ≤ b₂ coordinatewise, then dist(a₁, b₁) ≤ dist(a₂, b₂).

Русский

Если a₂ ≤ a₁ ≤ b₁ ≤ b₂ по каждой координате, то dist(a₁, b₁) ≤ dist(a₂, b₂).

LaTeX

$$$a_{2} \le a_{1} \le b_{1} \le b_{2} \implies \operatorname{dist}(a_{1}, b_{1}) \le \operatorname{dist}(a_{2}, b_{2})$$$

Lean4

theorem dist_mono_right_pi : MonotoneOn (dist x) (Ici x) := by
  simpa only [dist_comm _ x] using dist_mono_left_pi (y := x)

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