min'_singleton

Mathlib.Data.Finset.Max

URI: https://scilib.ai/kg/mathlib#Finset.min'_singleton

English

For a singleton {a}, the minimal element is a: min' of {a} equals a.

Русский

Для множества-одиночки {a} минимальный элемент равен a.

LaTeX

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

Lean4

/-- `{a}.min' _` is `a`. -/
@[simp]
theorem min'_singleton (a : α) : ({ a } : Finset α).min' (singleton_nonempty _) = a := by simp [min']

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

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

Разделы

Аффилиация

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