unbounded_gt_of_forall_exists_ge — Mathlib

English

If for every a there exists b ∈ s with b ≤ a, then Unbounded (>).

Русский

Если для каждого a существует b ∈ s с b ≤ a, то s неограничено по >.

LaTeX

$$([Preorder] (∀ a, ∃ b∈s, b ≤ a)) ⇒ Unbounded(>, s)$$

Lean4

theorem unbounded_gt_of_forall_exists_ge [Preorder α] (h : ∀ a, ∃ b ∈ s, b ≤ a) : Unbounded (· > ·) s := fun a =>
  let ⟨b, hb, hb'⟩ := h a
  ⟨b, hb, fun hba => not_le_of_gt hba hb'⟩

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