English
The range of mapRange is the set of all functions whose values lie in the range of e.
Русский
Образ mapRange состоит из всех функций, значения которых лежат в множестве range e.
LaTeX
$$Set.range (Finsupp.mapRange (α := α) e hf) = {g | ∀ i, g i ∈ Set.range e}$$
Lean4
theorem range_mapRange (e : M → N) (he₀ : e 0 = 0) :
Set.range (Finsupp.mapRange (α := α) e he₀) = {g | ∀ i, g i ∈ Set.range e} :=
by
ext g
simp only [Set.mem_range, Set.mem_setOf]
constructor
· rintro ⟨g, rfl⟩ i
simp
· intro h
classical
choose f h using h
use onFinset g.support (fun x ↦ if x ∈ g.support then f x else 0) (by simp_all)
ext i
simp only [mapRange_apply, onFinset_apply]
split_ifs <;> simp_all
