eqOn_mulIndicator — Mathlib

English

On the set s, mulIndicator s f equals f; i.e., for any x ∈ s, (mulIndicator s f)(x) = f(x).

Русский

На множестве s индикатор умножения равен самой функции f: для любого x ∈ s выполняется (mulIndicator s f)(x) = f(x).

LaTeX

$$$\\mathrm{EqOn}(\\mathrm{mulIndicator}(s,f), f, s)$$$

Lean4

/-- See `Set.eqOn_mulIndicator'` for the version with `sᶜ`. -/
@[to_additive /-- See `Set.eqOn_indicator'` for the version with `sᶜ`. -/
    ]
theorem eqOn_mulIndicator : EqOn (mulIndicator s f) f s := fun _ hx => mulIndicator_of_mem hx f

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