max_insert — Mathlib

English

For any a and finite s, the maximum of insert a s equals the maximum of a and s.max, i.e. (insert a s).max = max(ã, s.max).

Русский

Для любого a и конечного s максимум вставки a в s равен максимму a и s.max: (insert a s).max = max (a) s.max.

LaTeX

$$$$ \\operatorname{max}(\\operatorname{insert}(a,s)) = \\max( \\uparrow a, s.max). $$$$

Lean4

@[simp]
theorem max_insert {a : α} {s : Finset α} : (insert a s).max = max (↑a) s.max :=
  fold_insert_idem

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