lowerClosure — Mathlib

English

The least lower set containing a given set s is the set {x | ∃ a ∈ s, x ≤ a}.

Русский

Наименьшее нижнее множество, содержащее множество s, равно {x | ∃ a ∈ s, x ≤ a}.

LaTeX

$$$lowerClosure(s) = \\lbrace x \\mid ∃ a ∈ s, x \\le a \\rbrace$$$

Lean4

/-- The least lower set containing a given set. -/
def lowerClosure (s : Set α) : LowerSet α :=
  ⟨{x | ∃ a ∈ s, x ≤ a}, fun _ _ hle h => h.imp fun _x hx => ⟨hx.1, hle.trans hx.2⟩⟩
    -- TODO: move `GaloisInsertion`s up, use them to prove lemmas

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