instTop — Mathlib

English

The collection of submodules forms a lattice with a top element, the whole space.

Русский

Множество подпространств образует решетку с верхним элементом, равным всему пространству.

LaTeX

$$$\text{Submodule}_R(M)$ is a complete lattice with top element $\top$.$$

Lean4

/-- The universal set is the top element of the lattice of submodules. -/
instance : Top (Submodule R M) :=
  ⟨{ (⊤ : AddSubmonoid M) with
      carrier := Set.univ
      smul_mem' := fun _ _ _ ↦ trivial }⟩

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