finite_span_isCompactElement — Mathlib

English

The span of a finite subset is a compact element of the lattice of submodules.

Русский

Порожденный конечным подмножеством элемент компактен в решётке подмодулей.

LaTeX

$$$$ \\operatorname{IsCompactElement}(\\operatorname{span}_R(S)) \\,\\text{for finite } S. $$$$

Lean4

/-- The span of a finite subset is compact in the lattice of submodules. -/
theorem finite_span_isCompactElement (S : Set M) (h : S.Finite) :
    CompleteLattice.IsCompactElement (span R S : Submodule R M) :=
  Finite.coe_toFinset h ▸ finset_span_isCompactElement h.toFinset

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