isLeast_singleton

Mathlib.Order.Bounds.Basic

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

English

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

Русский

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

LaTeX

$$$ IsLeast\ { a \ }\ a $$$

Lean4

@[simp]
theorem isLeast_singleton : IsLeast { a } a :=
  @isGreatest_singleton αᵒᵈ _ a

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

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

Разделы

Аффилиация

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