lub_Iio_le

Mathlib.Order.Bounds.Basic

URI: https://scilib.ai/kg/mathlib#lub_Iio_le

English

If j is the LUB of Iio i, then j ≤ i.

Русский

Если j является наим. верхней границей множества Iio i, тогда j ≤ i.

LaTeX

$$$\forall {i j}, (IsLUB(Iio(i), j) \Rightarrow j ≤ i)$$$

Lean4

theorem lub_Iio_le (a : α) (hb : IsLUB (Iio a) b) : b ≤ a :=
  (isLUB_le_iff hb).mpr fun _ hk => le_of_lt hk

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

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

Разделы

Аффилиация

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