isLUB

Mathlib.Order.Bounds.Basic

URI: https://scilib.ai/kg/mathlib#IsGreatest.isLUB

English

If a is IsGreatest s a, then a is IsLUB s a.

Русский

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

LaTeX

$$IsGreatest\s a \Rightarrow IsLUB\s a$$

Lean4

theorem isLUB (h : IsGreatest s a) : IsLUB s a :=
  ⟨h.2, fun _ hb => hb h.1⟩

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

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

Разделы

Аффилиация

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