instIsCompactlyGenerated — Mathlib

English

The lattice of LieSubmodules is compactly generated: every LieSubmodule N is the supremum of lieSpan of elements of N.

Русский

Грань Лие-подмодуля компактно порождается: каждый N равен верхней грань lieSpan элементов N.

LaTeX

$$IsCompactlyGenerated (LieSubmodule R L M)$$

Lean4

instance instIsCompactlyGenerated : IsCompactlyGenerated (LieSubmodule R L M) :=
  ⟨fun N ↦
    ⟨(fun x ↦ lieSpan R L { x }) '' N, fun _ ⟨m, _, hm⟩ ↦ hm ▸ isCompactElement_lieSpan_singleton R L m,
      N.sSup_image_lieSpan_singleton⟩⟩

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