instCompleteSemilatticeInf — Mathlib

English

Compatibility of intersection and submodule underlying structure: s ⊓ t corresponds to s.toSubmodule ⊓ t.toSubmodule.

Русский

Совместимость пересечения и базовой структуры подмодуля: s ⊓ t соответствует s.toSubmodule ⊓ t.toSubmodule.

LaTeX

$$$\operatorname{toSubmodule}(s \cap t) = \operatorname{toSubmodule}(s) \cap \operatorname{toSubmodule}(t)$$$

Lean4

instance : CompleteSemilatticeInf (ClosedSubmodule R M)
    where
  sInf_le s a ha
    _ := by
    simp only [toSubmodule_sInf, Submodule.mem_iInf]
    exact fun h ↦ h a ha
  le_sInf s a ha
    b := by
    simp only [toSubmodule_sInf, Submodule.mem_iInf]
    exact fun a i hi ↦ ha i hi a

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