iSup_range_lsingle — Mathlib

English

The supremum over i of the ranges of lsingle i equals the top submodule.

Русский

Супремум по i от диапазонов lsingle i равен верхнему подполному.

LaTeX

$$$\\bigl\\langle \\bigl\\{\\mathrm{range}(\\mathrm{lsingle}\\ i)\\bigr\\}_{i}, \\top\\bigr\\rangle = \\top$$$

Lean4

theorem iSup_range_lsingle : ⨆ i, LinearMap.range (lsingle (R := R) (M := M) i) = ⊤ :=
  top_le_iff.mp fun m _ ↦ by
    rw [← LinearMap.id_apply (R := R) m, ← lsum_lsingle ℕ]
    exact dfinsuppSumAddHom_mem _ _ _ fun i _ ↦ Submodule.mem_iSup_of_mem i ⟨_, rfl⟩

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