English
If g is injective, then the indicator of the image g[S] with respect to f, evaluated at g(x), equals the indicator of S with respect to f ∘ g, evaluated at x.
Русский
Пусть g исчерпывающе инъективно; тогда индикатор образа g[S] относительно f в точке g(x) равен индикатору S относительно f ∘ g в точке x.
LaTeX
$${s : Set α} {f : β → M} {g : α → β} (hg : Injective g) {x : α} :\n mulIndicator (g '' s) f (g x) = mulIndicator s (f ∘ g) x$$
Lean4
@[to_additive]
theorem mulIndicator_image {s : Set α} {f : β → M} {g : α → β} (hg : Injective g) {x : α} :
mulIndicator (g '' s) f (g x) = mulIndicator s (f ∘ g) x := by
rw [← mulIndicator_comp_right, preimage_image_eq _ hg]