mrange_map — Mathlib

English

The range of the direct-sum map DirectSum.map f equals the comap of the pi-range of each f_i.

Русский

Образ отображения DirectSum.map f равен прообразу (comap) прямой суммы по единице pi от образов каждого f_i.

LaTeX

$$$\\mathrm{mrange}(\\mathrm{DirectSum.map} f) = \\big(\\mathrm{AddSubmonoid.pi}\\big(\\mathrm{Set.univ}, i \\mapsto \\mathrm{mrange}(f_i)\\big)\\big).\\mathrm{comap}\\big(\\mathrm{DirectSum.coeFnAddMonoidHom}\\,N\\big).$$$

Lean4

theorem mrange_map :
    AddMonoidHom.mrange (map f) =
      (AddSubmonoid.pi Set.univ (fun i ↦ AddMonoidHom.mrange (f i))).comap (coeFnAddMonoidHom N) :=
  DFinsupp.mrange_mapRangeAddMonoidHom f

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