mem_iSup_iff_exists_dfinsupp — Mathlib

English

Variant of the range description for mapRange.linearMap, emphasizing the coordinatewise ranges.

Русский

Вариант описания образа mapRange.linearMap, выделяющий координатные образы.

LaTeX

$$$\\mathrm{range}(\\mathrm{mapRange.linearMap}\\; f) = (\\mathrm{Submodule.pi}\\; \\mathrm{Set.univ}\\; (\\mathrm{range}\\; f_i)).\\mathrm{comap}\\; (\\mathrm{coeFnLinearMap}\\; R)$$$

Lean4

/-- A characterisation of the span of a family of submodules.

See also `Submodule.mem_iSup_iff_exists_finsupp`. -/
theorem mem_iSup_iff_exists_dfinsupp (p : ι → Submodule R N) (x : N) :
    x ∈ iSup p ↔ ∃ f : Π₀ i, p i, DFinsupp.lsum ℕ (fun i => (p i).subtype) f = x :=
  SetLike.ext_iff.mp (iSup_eq_range_dfinsupp_lsum p) x

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