mulSupport_mulIndicator — Mathlib

English

The indicator equals one exactly when the same disjointness holds: Disjoint (mulSupport f) s.

Русский

Индикатор равен единице тогда и только тогда, когда выполняется условие Disjoint (mulSupport f) s.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem mulSupport_mulIndicator : Function.mulSupport (s.mulIndicator f) = s ∩ Function.mulSupport f :=
  ext fun x => by simp [Function.mem_mulSupport, mulIndicator_apply_eq_one]

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