sup_eq_half_smul_add_add_abs_sub'

English

Similarly, x ⊔ y = (1/2) · (x + y + |y − x|) in the lattice context.

Русский

Аналогично, 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⁻¹ : 𝕜) • (x + y + |y - x|) :=
  let := invertibleOfNonzero (two_ne_zero' 𝕜);
  sup_eq_half_smul_add_add_abs_sub 𝕜 x y

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