upperClosure — Mathlib

English

The carrier of the upper closure equals the union of principal upper sets: ↑(upperClosure s) = ⋃ a ∈ s, Ici a.

Русский

носитель верхнего замыкания равен объединению мономножества верхних множеств: ↑(upperClosure s) = ⋃ a ∈ s, Ici a.

LaTeX

$$$↑(upperClosure\,s) = \\bigcup_{a \\in s} \\Ici a$$$

Lean4

/-- The greatest upper set containing a given set. -/
def upperClosure (s : Set α) : UpperSet α :=
  ⟨{x | ∃ a ∈ s, a ≤ x}, fun _ _ hle h => h.imp fun _x hx => ⟨hx.1, hx.2.trans hle⟩⟩

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