instCompleteLattice — Mathlib

English

The substructure generated by a set is the infimum of all substructures containing the set.

Русский

Подструктура, порождаемая множеством, является infimum всех подструктур, содержащих это множество.

LaTeX

$$$$ closure_L(s) = \inf \{ S : L.Substructure M \mid s \subseteq S \} $$$$

Lean4

/-- Substructures of a structure form a complete lattice. -/
instance instCompleteLattice : CompleteLattice (L.Substructure M) :=
  {
    completeLatticeOfInf (L.Substructure M) fun _ =>
      IsGLB.of_image (fun {S T : L.Substructure M} => show (S : Set M) ≤ T ↔ S ≤ T from SetLike.coe_subset_coe)
        isGLB_biInf with
    le := (· ≤ ·)
    lt := (· < ·)
    top := ⊤
    le_top := fun _ x _ => mem_top x
    inf := (· ⊓ ·)
    sInf := InfSet.sInf
    le_inf := fun _a _b _c ha hb _x hx => ⟨ha hx, hb hx⟩
    inf_le_left := fun _ _ _ => And.left
    inf_le_right := fun _ _ _ => And.right }

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