unbounded_gt_iff — Mathlib

English

In a linear order, unboundedness of GT is equivalent to a dual statement about ≤.

Русский

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

LaTeX

$$Unbounded(>, s) ⇔ ∀ a, ∃ b ∈ s, b ≤ a$$

Lean4

theorem unbounded_gt_iff [LinearOrder α] : Unbounded (· > ·) s ↔ ∀ a, ∃ b ∈ s, b ≤ a :=
  ⟨fun h a =>
    let ⟨b, hb, hba⟩ := h a
    ⟨b, hb, le_of_not_gt hba⟩,
    unbounded_gt_of_forall_exists_ge⟩

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