min_insert

Mathlib.Data.Finset.Max

URI: https://scilib.ai/kg/mathlib#Finset.min_insert

English

The minimum of insert a s is the minimum of a and s.min.

Русский

Минимум (insert a s) равен min(a, s.min).

LaTeX

$$$\min(\text{insert } a\ s) = \min(a, s.min)$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru