unbounded_ge_of_forall_exists_gt — Mathlib

English

If for every a there exists b ∈ s with b < a, then s is unbounded for ≥; conversely, this implies the forward direction.

Русский

Если для каждого a существует b в s с b < a, тогда s неограничено по ≥; обратно это следует из дуальной связи.

LaTeX

$$Unbounded(≥, s) ⇔ (∀ a, ∃ b∈s, b < a)$$

Lean4

theorem unbounded_ge_of_forall_exists_gt [Preorder α] (h : ∀ a, ∃ b ∈ s, b < a) : Unbounded (· ≥ ·) s :=
  @unbounded_le_of_forall_exists_lt αᵒᵈ _ _ h

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