unbounded_gt_iff_unbounded_ge

Mathlib.Order.Bounded

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

← MathLib Explorer

English

There is a duality: LT-unboundedness is equivalent to GE-unboundedness.

Русский

Существует дуальность: LT-неограниченность эквивалентна GE-неограниченности.

LaTeX

$$Unbounded( LT, s ) ⇔ Unbounded( GE, s )$$

Lean4

theorem unbounded_gt_iff_unbounded_ge [Preorder α] [NoMinOrder α] : Unbounded (· > ·) s ↔ Unbounded (· ≥ ·) s :=
  @unbounded_lt_iff_unbounded_le αᵒᵈ _ _ _

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

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

Разделы

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

Аффилиация

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