maximum_mem — Mathlib

English

If the maximum of a list l is m (as a WithBot value), then m is an element of l.

Русский

Если максимум списка l равен m (как значение WithBot), то m является элементом списка l.

LaTeX

$$$\forall l.\; \forall m.\; (\operatorname{maximum} l : \mathrm{WithBot}\; \alpha) = \operatorname{WithBot}.some(m) \rightarrow m \in l$$$

Lean4

theorem maximum_mem {l : List α} {m : α} : (maximum l : WithTop α) = m → m ∈ l :=
  argmax_mem

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