mapRange_smul — Mathlib

English

Range of the coordinatewise mapRange.addMonoidHom equals the comap of coordinate-wise ranges.

Русский

Диапазон отображения mapRange.addMonoidHom по координатам равен прообразу диапазонов по каждой координате.

LaTeX

$$$\\mathrm{mrange}(\\mathrm{mapRange}.addMonoidHom f) = (\\mathrm{AddSubmonoid.pi}\\; Set.univ (\\lambda i, \\mathrm{mrange}(f_i))).\\mathrm{comap}\\; \\mathrm{coeFnAddMonoidHom}$$$

Lean4

theorem mapRange_smul (f : ∀ i, β₁ i → β₂ i) (hf : ∀ i, f i 0 = 0) (r : R) (hf' : ∀ i x, f i (r • x) = r • f i x)
    (g : Π₀ i, β₁ i) : mapRange f hf (r • g) = r • mapRange f hf g :=
  by
  ext
  simp only [mapRange_apply f, coe_smul, Pi.smul_apply, hf']

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