closure — Mathlib

English

The generated substructure includes the original set: s ⊆ closure L s.

Русский

Порождаемая подструктура включает исходное множество: s ⊆ closure_L(s).

LaTeX

$$$$ s \subseteq closure_L(s) $$$$

Lean4

/-- The `L.Substructure` generated by a set. -/
def closure : LowerAdjoint ((↑) : L.Substructure M → Set M) :=
  ⟨fun s => sInf {S | s ⊆ S}, fun _ _ =>
    ⟨Set.Subset.trans fun _x hx => mem_sInf.2 fun _S hS => hS hx, fun h => sInf_le h⟩⟩

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