mker_mapRangeAddMonoidHom — Mathlib

English

Variant statement asserting the same top-range property with possibly different indexing assumptions.

Русский

Вариант утверждения той же верхней границы множества образов.

LaTeX

$$$\\bigl( \\text{range}(\\mathrm{lsingle}) \\bigr)^{\\uparrow} = \\top$$$

Lean4

theorem mker_mapRangeAddMonoidHom (f : ∀ i, β₁ i →+ β₂ i) :
    AddMonoidHom.mker (mapRange.addMonoidHom f) =
      (AddSubmonoid.pi Set.univ (fun i ↦ AddMonoidHom.mker (f i))).comap coeFnAddMonoidHom :=
  by
  ext
  simp [AddSubmonoid.pi, DFinsupp.ext_iff]

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