not_bddBelow

Mathlib.Order.UpperLower.Basic

URI: https://scilib.ai/kg/mathlib#IsLowerSet.not_bddBelow

← MathLib Explorer

English

There is no upper bound for the open ray Ioi a.

Русский

Для множества Ioi a не существует верхней границы.

LaTeX

$$not_bddAbove_Ioi (a) : ¬BddAbove (Ioi a)$$

Lean4

theorem not_bddBelow (hs : IsLowerSet s) : s.Nonempty → ¬BddBelow s :=
  by
  rintro ⟨a, ha⟩ ⟨b, hb⟩
  obtain ⟨c, hc⟩ := exists_lt b
  exact hc.not_ge (hb <| hs (hc.le.trans <| hb ha) ha)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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