isGLB

Mathlib.Order.Bounds.Basic

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

English

If a is IsLeast s a, then a is IsGLB s a.

Русский

Если a является наименьшей верхней границей множества s, то a является наибольшей нижней границей s.

LaTeX

$$IsLeast\ s a \Rightarrow IsGLB\ s a$$

Lean4

theorem isGLB (h : IsLeast s a) : IsGLB s a :=
  ⟨h.2, fun _ hb => hb h.1⟩

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

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

Разделы

Аффилиация

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