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⟩