mulIndicator_self_mul_compl_apply

English

For any s ⊆ α and f: α → M, mulIndicator s f a · mulIndicator sᶜ f a = f a for all a ∈ α. The product of the two complementary indicators yields the original value.

Русский

Для любой пары индикаторов s и его комплемента на точке a произведение равно f(a).

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem mulIndicator_self_mul_compl_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]

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