sSup_image_lieSpan_singleton — Mathlib

English

For a LieSubmodule N, the supremum of the Lie-span of singletons of elements of N equals N itself: sSup { lieSpan{m} : m ∈ N } = N.

Русский

Для Lie-подмодуля N верхняя грань объединения {lieSpan{m} | m ∈ N} равна N.

LaTeX

$$sSup_{LieSubmodule}( { lieSpan_{R,L}({m}) : m ∈ N } ) = N$$

Lean4

@[simp]
theorem sSup_image_lieSpan_singleton : sSup ((fun x ↦ lieSpan R L { x }) '' N) = N :=
  by
  refine le_antisymm (sSup_le <| by simp) ?_
  simp_rw [← toSubmodule_le_toSubmodule, sSup_toSubmodule, Set.mem_image, SetLike.mem_coe]
  refine fun m hm ↦ Submodule.mem_sSup.mpr fun N' hN' ↦ ?_
  replace hN' : ∀ m ∈ N, lieSpan R L { m } ≤ N' := by simpa using hN'
  exact hN' _ hm (subset_lieSpan rfl)

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