mulIndicator_self_mul_compl — Mathlib

English

For any s ⊆ α and f: α → M, mulIndicator s f · mulIndicator sᶜ f = f as a function α → M. The two indicators multiply to recover f.

Русский

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

LaTeX

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

Lean4

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

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