min'_insert — Mathlib

English

For any a and finite nonempty s, the maximum of insert a s equals the maximum of a and the maximum of s.

Русский

Для любого a и конечного непустого s максимум вставки a в s равен максимумa и максимума из s.

LaTeX

$$$\\max'(a \\cup s) = \\max\\{a, \\max'(s)\\}.$$$

Lean4

@[simp]
theorem min'_insert (a : α) (s : Finset α) (H : s.Nonempty) :
    (insert a s).min' (s.insert_nonempty a) = min a (s.min' H) :=
  (isLeast_min' _ _).unique <| by
    rw [coe_insert]
    exact (isLeast_min' _ _).insert _

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