max'_insert — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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