mulIndicator_range_comp — Mathlib

English

Let f be a function from an index set ι into α, and g: α → M. Then the function obtained by applying g only on the range of f and otherwise returning the multiplicative unit is unchanged after precomposing with f; i.e., (mulIndicator(range f) g) ∘ f = g ∘ f.

Русский

Пусть f: ι → α и g: α → M. Тогда применение функции-индикатора к диапазону образа f не изменяет композицию с f: (mulIndicator(range f) g) ∘ f = g ∘ f.

LaTeX

$$$$(\mathrm{mulIndicator}(\mathrm{range}(f))\ g) \circ f = g \circ f.$$$$

Lean4

@[to_additive (attr := simp)]
theorem mulIndicator_range_comp {ι : Sort*} (f : ι → α) (g : α → M) : mulIndicator (range f) g ∘ f = g ∘ f :=
  letI := Classical.decPred (· ∈ range f)
  piecewise_range_comp _ _ _

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