mulIndicator_inv — Mathlib

English

For a Set s and a function f: α → G with G a Group, mulIndicator s (f)⁻¹ equals (mulIndicator s f)⁻¹. This is a restatement via the inverse property.

Русский

Для множества s и функции f: α → G, индикатор на f⁻¹ равен инверсии индикатора на f.

LaTeX

$$$$ \\forall s:\\ Set\\,\\alpha, f:\\alpha \\to G,\\ mulIndicator s (f)^{-1} = (mulIndicator s f)^{-1} $$$$

Lean4

@[to_additive]
theorem mulIndicator_inv (s : Set α) (f : α → G) :
    (mulIndicator s fun a => (f a)⁻¹) = fun a => (mulIndicator s f a)⁻¹ :=
  mulIndicator_inv' s f

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