exists_ge — Mathlib

English

In a semilattice with sup, if s is bounded above, then for every x₀ there exists x such that x₀ ≤ x and all elements of s are ≤ x.

Русский

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

LaTeX

$$$[SemilatticeSup γ] {s : Set γ} (hs : BddAbove s) (x₀ : γ) : ∃ x, x₀ \le x ∧ ∀ y ∈ s, y \le x$$$

Lean4

theorem exists_ge [SemilatticeSup γ] {s : Set γ} (hs : BddAbove s) (x₀ : γ) : ∃ x, x₀ ≤ x ∧ ∀ y ∈ s, y ≤ x :=
  (bddAbove_iff_exists_ge x₀).mp hs

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