mapRange_single — Mathlib

English

Applying mapRange to a single coordinate preserves the singleton form on the image.

Русский

Применение mapRange к одиночной координате сохраняет форму одинарного элемента на изображении.

LaTeX

$$$\\mathrm{mapRange}\,f\,hf\, (\\mathrm{single}_i b) = \\mathrm{single}_i (f_i b)$$$

Lean4

@[simp]
theorem mapRange_single {f : ∀ i, β₁ i → β₂ i} {hf : ∀ i, f i 0 = 0} {i : ι} {b : β₁ i} :
    mapRange f hf (single i b) = single i (f i b) :=
  DFinsupp.ext fun i' => by
    by_cases h : i = i'
    · subst i'
      simp
    · simp [h, hf]

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