min_apply — Mathlib

English

The pointwise minimum of two LocallyFinsuppWithin elements, evaluated at x, equals the minimum of their evaluations at x.

Русский

Точечное минимума двух элементов LocallyFinsuppWithin при x равно минимума их значений при x.

LaTeX

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

Lean4

@[simp]
theorem min_apply [SemilatticeInf Y] [Zero Y] {D₁ D₂ : locallyFinsuppWithin U Y} {x : X} :
    min D₁ D₂ x = min (D₁ x) (D₂ x) :=
  rfl

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