instCompleteSemilatticeSup — Mathlib

English

The toSubmodule of the supremum over S equals the closure of the supremum of the submodules.

Русский

toSubmodule(sSup S) равно замыканию супа подмодулей.

LaTeX

$$$toSubmodule( sSup S ) = (\bigvee S).closure.toSubmodule$$$

Lean4

instance : CompleteSemilatticeSup (ClosedSubmodule R N)
    where
  le_sSup s a ha x hx := subset_closure <| Submodule.mem_iSup_of_mem _ <| Submodule.mem_iSup_of_mem ha hx
  sSup_le s a h
    x := by
    rw [← ClosedSubmodule.closure_toSubmodule_eq (s := a)]
    apply closure_mono
    simp only [Submodule.coe_toAddSubmonoid, coe_toSubmodule]
    intro y hy
    simp only [SetLike.mem_coe, Submodule.mem_iSup] at hy
    exact hy a fun b _ hz ↦ Submodule.mem_iSup _ |>.mp hz _ <| fun hb ↦ h b hb

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