lowerBounds_eq

Mathlib.Order.Bounds.Basic

URI: https://scilib.ai/kg/mathlib#IsLeast.lowerBounds_eq

English

If h is IsLeast s a, then lowerBounds s = Iic a.

Русский

Если a является наименьшей нижней границей множества s, то нижние границы s равны множеству {x | x ≤ a}.

LaTeX

$$IsLeast\ s a \Rightarrow lowerBounds\ s = Iic(a)$$

Lean4

theorem lowerBounds_eq (h : IsLeast s a) : lowerBounds s = Iic a :=
  h.isGLB.lowerBounds_eq

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

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

Разделы

Аффилиация

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