bounded_ge_of_bounded_gt

Mathlib.Order.Bounded

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

English

If GT-boundedness holds on s, then GE-boundedness holds on s.

Русский

Если множество ограничено по GT, то ограничено по GE.

LaTeX

$$GT_bounded(s) ⇒ GE_bounded(s)$$

Lean4

theorem bounded_ge_of_bounded_gt [Preorder α] (h : Bounded (· > ·) s) : Bounded (· ≥ ·) s :=
  let ⟨a, ha⟩ := h
  ⟨a, fun b hb => le_of_lt (ha b hb)⟩

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

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

Разделы

Аффилиация

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