inf_eq_half_smul_add_sub_abs_sub'

English

Same as 25793 but in a broader scalar context: x ⊓ y = (1/2)·(x + y − |y − x|) for appropriate scalar field 𝕜.

Русский

Та же формула для инфимума, но в другом скаляровом контексте: x ⊓ y = (1/2)·(x + y − |y − x|).

LaTeX

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

Lean4

theorem inf_eq_half_smul_add_sub_abs_sub' (x y : M) : x ⊓ y = (2⁻¹ : 𝕜) • (x + y - |y - x|) :=
  let := invertibleOfNonzero (two_ne_zero' 𝕜);
  inf_eq_half_smul_add_sub_abs_sub 𝕜 x y

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