finset_span_isCompactElement — Mathlib

English

The span of a finite set is compact in the lattice of submodules.

Русский

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

LaTeX

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

Lean4

/-- The span of a finite subset is compact in the lattice of submodules. -/
theorem finset_span_isCompactElement (S : Finset M) : CompleteLattice.IsCompactElement (span R S : Submodule R M) :=
  by
  rw [span_eq_iSup_of_singleton_spans]
  simp only [Finset.mem_coe]
  rw [← Finset.sup_eq_iSup]
  exact CompleteLattice.isCompactElement_finsetSup S fun x _ => singleton_span_isCompactElement x

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