unbounded_ge_iff — Mathlib

English

In a linear order, unboundedness of ≥ is equivalent to a dual statement about lt via the dual order.

Русский

В линейном порядке неограниченность ≥ эквивалентна двойственному утверждению о lt в двойственном порядке.

LaTeX

$$Unbounded(≥, s) ⇔ Unbounded(<, s) в OrderDual$$

Lean4

theorem unbounded_ge_iff [LinearOrder α] : Unbounded (· ≥ ·) s ↔ ∀ a, ∃ b ∈ s, b < a :=
  ⟨fun h a =>
    let ⟨b, hb, hba⟩ := h a
    ⟨b, hb, lt_of_not_ge hba⟩,
    unbounded_ge_of_forall_exists_gt⟩

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