mulIndicator_compl_mul_self — Mathlib

English

For any s ⊆ α and f: α → M, mulIndicator sᶜ f · mulIndicator s f = f as a function α → M. In other words, the product of the complement indicator and the set indicator recovers the original function.

Русский

Для любого s ⊆ α и функции f: α → M произведение индикаторов комплемента и индикатора множества даёт исходную функцию f.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem mulIndicator_compl_mul_self (s : Set α) (f : α → M) : mulIndicator sᶜ f * mulIndicator s f = f :=
  funext <| mulIndicator_compl_mul_self_apply s f

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