comp_mulIndicator_const — Mathlib

English

If f(1) = 1, then f applied to the indicator of a constant c equals the indicator of the constant f(c).

Русский

Если f(1) = 1, то f( s.mulIndicator (константа c) ) = s.mulIndicator (константа f(c)).

LaTeX

$${c : M} (f : M → N) (hf : f 1 = 1) :\n (x \\mapsto f (s.mulIndicator (\\lambda _ => c) x)) = s.mulIndicator (\\lambda x => f c)$$

Lean4

@[to_additive]
theorem comp_mulIndicator_const (c : M) (f : M → N) (hf : f 1 = 1) :
    (fun x => f (s.mulIndicator (fun _ => c) x)) = s.mulIndicator fun _ => f c :=
  (mulIndicator_comp_of_one hf).symm

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