sup_eq_half_smul_add_add_abs_sub — Mathlib

English

In a lattice-ordered module, the supremum x ∨ y equals (1/2) · (x + y + |y − x|).

Русский

В упорядоченном по сетке модуле верхняя граница: x ∨ y = (1/2)·(x + y + |y − x|).

LaTeX

$$$ x \\vee y = \\left( \\tfrac{1}{2} \\right) \\cdot \\bigl( x + y + |y - x| \\bigr). $$$

Lean4

theorem sup_eq_half_smul_add_add_abs_sub (x y : M) : x ⊔ y = (⅟2 : R) • (x + y + |y - x|) := by
  rw [← two_nsmul_sup_eq_add_add_abs_sub x y, two_smul, ← two_smul R, smul_smul, invOf_mul_self, one_smul]

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