dist_mono_left_pi — Mathlib

English

Analogous to the left version, the map x ↦ dist(x, y) is monotone on ICI y coordinatewise.

Русский

Аналогично левой версии, отображение x ↦ dist(x, y) монотонно по координатам, когда x растёт.

LaTeX

$$$\text{MonotoneOn } (\mathrm{dist}(x, \cdot)) \; (\, \mathrm{Ici} \; x\,)$$$

Lean4

theorem dist_mono_left_pi : MonotoneOn (dist · y) (Ici y) :=
  by
  refine fun y₁ hy₁ y₂ hy₂ hy ↦ NNReal.coe_le_coe.2 (Finset.sup_mono_fun fun i _ ↦ ?_)
  rw [Real.nndist_eq, Real.nnabs_of_nonneg (sub_nonneg_of_le (‹y ≤ _› i : y i ≤ y₁ i)), Real.nndist_eq,
    Real.nnabs_of_nonneg (sub_nonneg_of_le (‹y ≤ _› i : y i ≤ y₂ i))]
  grw [hy i] -- TODO(gcongr): we would like `grw [hy]` to work here

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