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