bounded_lt_Iio

Mathlib.Order.Bounded

URI: https://scilib.ai/kg/mathlib#Set.bounded_lt_Iio

English

For any a in α, the set { x ∈ α | x < a } is bounded above with respect to <.

Русский

Для каждого a ∈ α множество { x ∈ α | x < a } ограничено сверху относительно отношения <.

LaTeX

$$$\forall a:\ Bound\ ed\ (<)\ (Iio\ a)$$$

Lean4

theorem bounded_lt_Iio [Preorder α] (a : α) : Bounded (· < ·) (Iio a) :=
  bounded_self a

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

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

Разделы

Аффилиация

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