norm_sup_sub_sup_le_norm

Mathlib.Analysis.Normed.Order.Lattice

URI: https://scilib.ai/kg/mathlib#norm_sup_sub_sup_le_norm

English

For x,y,z in α, ‖x ⊔ z − y ⊔ z‖ ≤ ‖x − y‖.

Русский

Для x,y,z в α верно ‖x ⊔ z − y ⊔ z‖ ≤ ‖x − y‖.

LaTeX

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

Lean4

theorem norm_sup_sub_sup_le_norm (x y z : α) : ‖x ⊔ z - y ⊔ z‖ ≤ ‖x - y‖ :=
  solid (abs_sup_sub_sup_le_abs x y z)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru