max_apply — Mathlib

English

The value of the pointwise maximum of two LocallyFinsuppWithin elements at a point x equals the maximum of their values at x.

Русский

Значение точечного максимума двух элементов LocallyFinsuppWithin в точке x равно максимуму их значений в x.

LaTeX

$$$\\max D_1 D_2 x = \\max\\big(D_1 x, D_2 x\\big)$$$

Lean4

@[simp]
theorem max_apply [SemilatticeSup Y] [Zero Y] {D₁ D₂ : locallyFinsuppWithin U Y} {x : X} :
    max D₁ D₂ x = max (D₁ x) (D₂ x) :=
  rfl

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