max'_singleton

Mathlib.Data.Finset.Max

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

English

For a singleton {a}, max' of it equals a.

Русский

Для множества-одиночки {a} максимум max' равен a.

LaTeX

$$$$\max'\{a\} = a.$$$$

Lean4

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

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

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

Разделы

Аффилиация

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