norm_inf_sub_inf_le_norm — Mathlib

English

Let α be a normed lattice-ordered additive group with a solid norm and compatible order. For all x, y, z in α we have ‖x ⊓ z − y ⊓ z‖ ≤ ‖x − y‖; i.e., the infimum with a fixed z is 1-Lipschitz in x and y.

Русский

Пусть α является нормируемым пространством с решёткой, имеет твердую норму и совместимый порядок. Тогда для любых x, y, z ∈ α выполняется ‖x ⊓ z − y ⊓ z‖ ≤ ‖x − y‖; т. е. операция взятия наименьшего элемента с фиксированным z не увеличивает расстояние (1‑липшицево).

LaTeX

$$$\|x \wedge z - y \wedge z\| \le \|x - y\|$$$

Lean4

theorem norm_inf_sub_inf_le_norm (x y z : α) : ‖x ⊓ z - y ⊓ z‖ ≤ ‖x - y‖ :=
  solid (abs_inf_sub_inf_le_abs x y z)

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