instSemilatticeSup — Mathlib

English

If N is a T1 space, then ClosedSubmodule R N forms a complete lattice.

Русский

Если N является T1-пространством, то ClosedSubmodule R N образует полную решётку.

LaTeX

$$$\text{CompleteLattice}(\text{ClosedSubmodule } R N)\quad\text{при } T1Space(N)$$$

Lean4

instance : SemilatticeSup (ClosedSubmodule R N) where
  sup s t := s ⊔ t
  le_sup_left _ _ _ hx := subset_closure <| Submodule.mem_sup_left hx
  le_sup_right _ _ _ hx := subset_closure <| Submodule.mem_sup_right hx
  sup_le _ _ _ ha hb := Submodule.closure_le.mpr <| sup_le_iff.mpr ⟨ha, hb⟩

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