mulIndicator_eq_one' — Mathlib

English

The multiplicative indicator equals 1 exactly when the support of f is disjoint from s.

Русский

Умножаемый индикатор равен единице тогда и только тогда, когда опора функции f не пересекается с множеством s.

LaTeX

$$$\\mathrm{mulIndicator}(s,f) = 1 \\iff \\mathrm{Disjoint}(\\mathrm{mulSupport}(f),s)$$$

Lean4

@[to_additive (attr := simp)]
theorem mulIndicator_eq_one' : mulIndicator s f = 1 ↔ Disjoint (mulSupport f) s :=
  mulIndicator_eq_one

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