English
If the supports of f and g are disjoint, then on the left side, (mulIndicator (mulSupport f) (f·g)) equals f.
Русский
Если множества поддержки функций f и g не пересекаются, то на левой стороне (mulIndicator (mulSupport f) (f·g)) равняется f.
LaTeX
$$$$ \\text{If } \\operatorname{Disjoint}(\\operatorname{mulSupport} f, \\operatorname{mulSupport} g), \\ (\\operatorname{mulIndicator}(\\operatorname{mulSupport} f))(f\\cdot g) = f. $$$$
Lean4
@[to_additive]
theorem mulIndicator_mul_eq_left {f g : α → M} (h : Disjoint (mulSupport f) (mulSupport g)) :
(mulSupport f).mulIndicator (f * g) = f :=
by
refine (mulIndicator_congr fun x hx => ?_).trans mulIndicator_mulSupport
have : g x = 1 := notMem_mulSupport.1 (disjoint_left.1 h hx)
rw [Pi.mul_apply, this, mul_one]
