isLeast_l

Mathlib.Order.GaloisConnection.Basic

URI: https://scilib.ai/kg/mathlib#GaloisConnection.isLeast_l

English

For any a in α, the set {b | a ≤ u b} has l a as its least element under l.

Русский

Для любого a из α множество {b | a ≤ u b} имеет наименьший элемент под действием l равный l a.

LaTeX

$$$$ IsLeast\\{b\\mid a \\le u b\\} \\; (l a) $$$$

Lean4

theorem isLeast_l {a : α} : IsLeast {b | a ≤ u b} (l a) :=
  ⟨gc.le_u_l _, fun _ hb => gc.l_le hb⟩

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

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

Разделы

Аффилиация

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