instInfSet — Mathlib

English

The submodules of M form a complete lattice under inclusion, with join given by the sum and meet by intersection.

Русский

Подмодули M образуют полную решетку по включению; сумма даёт объединение, пересечение — пересечение.

LaTeX

$$$\mathrm{Submodule}_R(M)$ is a complete lattice with join $p \vee q = p + q$ and meet $p \wedge q = p \cap q$.$$

Lean4

instance : InfSet (Submodule R M) :=
  ⟨fun S ↦
    { carrier := ⋂ s ∈ S, (s : Set M)
      zero_mem' := by simp [zero_mem]
      add_mem' := by simp +contextual [add_mem]
      smul_mem' := by simp +contextual [smul_mem] }⟩

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