unbounded_gt_of_unbounded_ge

Mathlib.Order.Bounded

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

← MathLib Explorer

English

If GE is unbounded on s, then GT is unbounded on s.

Русский

Если GE неограничено на s, то GT неограничено на s.

LaTeX

$$Unbounded(GT, s) from Unbounded(GE, s)$$

Lean4

theorem unbounded_gt_of_unbounded_ge [Preorder α] (h : Unbounded (· ≥ ·) s) : Unbounded (· > ·) s := fun a =>
  let ⟨b, hb, hba⟩ := h a
  ⟨b, hb, fun hba' => hba (le_of_lt hba')⟩

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

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

Разделы

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

Аффилиация

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