upperBounds_supClosure — Mathlib

English

The upper bounds of supClosure(s) are exactly the upper bounds of s.

Русский

верхние границы supClosure(s) совпадают с верхними границами s.

LaTeX

$$$\\mathrm{upperBounds}(\\operatorname{supClosure}(s)) = \\mathrm{upperBounds}(s)$$$

Lean4

@[simp]
theorem upperBounds_supClosure (s : Set α) : upperBounds (supClosure s) = upperBounds s :=
  (upperBounds_mono_set subset_supClosure).antisymm <|
    by
    rintro a ha _ ⟨t, ht, hts, rfl⟩
    exact sup'_le _ _ fun b hb ↦ ha <| hts hb

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