isGreatest_singleton

Mathlib.Order.Bounds.Basic

URI: https://scilib.ai/kg/mathlib#isGreatest_singleton

English

The singleton {a} has a as its greatest element.

Русский

Единственный элемент множества {a} является наибольшим элементом.

LaTeX

$$$ IsGreatest\ { a \ }\ a $$$

Lean4

@[simp]
theorem isGreatest_singleton : IsGreatest { a } a :=
  ⟨mem_singleton a, fun _ hx => le_of_eq <| eq_of_mem_singleton hx⟩

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

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

Разделы

Аффилиация

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