lowerBounds_upperClosure — Mathlib

English

For any preorder, the set of lower bounds of the upper closure of a subset s coincides with the set of lower bounds of s.

Русский

Для любого частично упорядоченного множества и подмножества s ⊆ α множества нижних границ верхнего замыкания s совпадают с множеством нижних границ самого s.

LaTeX

$$$ \\operatorname{lowerBounds}(\\operatorname{upperClosure}(s)) = \\operatorname{lowerBounds}(s) $$$

Lean4

@[simp]
theorem lowerBounds_upperClosure : lowerBounds (upperClosure s : Set α) = lowerBounds s :=
  (lowerBounds_mono_set subset_upperClosure).antisymm fun _a ha _b ⟨_c, hc, hcb⟩ ↦ (ha hc).trans hcb

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