singleton_span_isCompactElement — Mathlib

English

The span of a single vector is a compact element in the lattice of submodules.

Русский

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

LaTeX

$$$$ \\operatorname{IsCompactElement}(\\operatorname{span}_R(\\{x\\})) $$$$

Lean4

theorem singleton_span_isCompactElement (x : M) : CompleteLattice.IsCompactElement (span R { x } : Submodule R M) :=
  by
  rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le]
  intro d hemp hdir hsup
  have : x ∈ (sSup d) := (SetLike.le_def.mp hsup) (mem_span_singleton_self x)
  obtain ⟨y, ⟨hyd, hxy⟩⟩ := (mem_sSup_of_directed hemp hdir).mp this
  exact ⟨y, ⟨hyd, by simpa only [span_le, singleton_subset_iff]⟩⟩

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