lowerBounds_univ — Mathlib

English

In any partially ordered set with a bottom element, the set of lower bounds of the entire universe is exactly the singleton {⊥}.

Русский

В любом частично упорядоченном множестве, имеющем нижнюю границу ⊥, множество нижних границ всего множества равно {⊥}.

LaTeX

$$$\\operatorname{lowerBounds}(\\mathrm{univ}) = \\{ \\bot \\}$$$

Lean4

@[simp]
theorem lowerBounds_univ [PartialOrder γ] [OrderBot γ] : lowerBounds (univ : Set γ) = {⊥} :=
  @OrderTop.upperBounds_univ γᵒᵈ _ _

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