mulIndicator_comp_right — Mathlib

English

For any a function f: β → α, and g: α → M, and x ∈ β, the preimage of mulIndicator (f^{-1}(S)) (g ∘ f) at x equals mulIndicator S g at f(x).

Русский

Для любой отображения f: β → α и g: α → M и элемента x, предобраз mulIndicator (f^{-1}(S)) от (g ∘ f) в x равен mulIndicator S g в f(x).

LaTeX

$${s : Set α} (f : β → α) {g : α → M} {x : β} :\n (f^{-1} s).mulIndicator (g ∘ f) x = s.mulIndicator g (f x)$$

Lean4

@[to_additive]
theorem mulIndicator_comp_right {s : Set α} (f : β → α) {g : α → M} {x : β} :
    mulIndicator (f ⁻¹' s) (g ∘ f) x = mulIndicator s g (f x) := by tauto

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