mulIndicator — Mathlib

English

If a function f: β → α is Multipliable, then for every subset s ⊆ β, the indicator of f on s (equal to f on s and to the neutral element outside s) is Multipliable.

Русский

Если функция f: β → α суммируема по умножению, то для любого подмножества s ⊆ β индикаторная функция f на s (равная f на s и единице вне s) также суммируема.

LaTeX

$$$$\\text{Multipliable}(f) \\rightarrow \\forall s \\subseteq \\beta,\\ \\text{Multipliable}(s.\\mathrm{mulIndicator}(f)).$$$$

Lean4

@[to_additive]
protected theorem mulIndicator (hf : Multipliable f) (s : Set β) : Multipliable (s.mulIndicator f) :=
  hf.multipliable_of_eq_one_or_self <| Set.mulIndicator_eq_one_or_self _ _

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