mulIndicator_compl' — Mathlib

English

For any s and f, mulIndicator sᶜ f · mulIndicator s f = f. The product of complementary indicators recovers f.

Русский

Произведение индикаторов комплемента и индикатора множества восстанавливает f.

LaTeX

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

Lean4

@[to_additive indicator_compl]
theorem mulIndicator_compl' (s : Set α) (f : α → G) : mulIndicator sᶜ f = f / mulIndicator s f := by
  rw [div_eq_mul_inv, mulIndicator_compl]

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