bddAbove_iff_exists_ge — Mathlib

English

For a semilattice with sup, if s is bounded above, then for any x₀ there exists an element x above x₀ that dominates all elements of s.

Русский

В полулинейком множестве с верхней границей существует элемент x выше заданного x₀, который доминирует все элементы множества s.

LaTeX

$$$[SemilatticeSup γ] {s : Set γ} (hs : BddAbove s) (x₀ : γ) : \exists x, x₀ \le x \land \forall y \in s, y \le x$$$

Lean4

theorem bddAbove_iff_exists_ge [SemilatticeSup γ] {s : Set γ} (x₀ : γ) : BddAbove s ↔ ∃ x, x₀ ≤ x ∧ ∀ y ∈ s, y ≤ x :=
  by
  rw [bddAbove_def, exists_ge_and_iff_exists]
  exact Monotone.ball fun x _ => monotone_le

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