mulIndicator_image — Mathlib

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]

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