max_singleton

Mathlib.Data.Finset.Max

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

English

For any a in a linear order, max of the singleton {a} is a, i.e. Finset.max {a} = a expressed in WithBot.

Русский

Для любого a в линейном порядке максимум множества {a} есть a: Finset.max {a} = a.

LaTeX

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

Lean4

@[simp]
theorem max_singleton {a : α} : Finset.max { a } = (a : WithBot α) :=
  by
  rw [← insert_empty_eq]
  exact max_insert

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

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

Разделы

Аффилиация

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