mulIndicator_compl_mul_self_apply

English

For any a ∈ α, the product of the indicator of the complement sᶜ and the indicator of s applied to f at a equals f(a). In other words, mulIndicator sᶜ f a · mulIndicator s f a = f a.

Русский

Для любого a ∈ α произведение индикаторов комплемента sᶜ и множества s, применённое к f, на точке a равно f(a). То есть mulIndicator sᶜ f a · mulIndicator s f a = f a.

LaTeX

$$$$ \\forall s: Set\\,\\alpha, f: \\alpha \\to M, a: \\alpha,\\quad mulIndicator s^c\,f\,a \\cdot mulIndicator s\,f\,a = f\\,a $$$$

Lean4

@[to_additive (attr := simp)]
theorem mulIndicator_compl_mul_self_apply (s : Set α) (f : α → M) (a : α) :
    mulIndicator sᶜ f a * mulIndicator s f a = f a :=
  by_cases (fun ha : a ∈ s => by simp [ha]) fun ha => by simp [ha]

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