English
The almost everywhere equality of the indicator s.mulIndicator f with 1 is equivalent to μ(s ∩ f.mulSupport) = 0.
Русский
Пусть f: α → M с единичным нейтральным элементом; тогда s.mulIndicator f = 1 почти по μ тогда и только тогда, μ(s ∩ supp(f)) = 0.
LaTeX
$$$ (s.mulIndicator f) =_{\mathrm{ae}}^{\mu} 1 \;\iff\; \mu (s \cap f.mulSupport) = 0 $$$
Lean4
@[to_additive]
theorem _root_.Set.mulIndicator_ae_eq_one {M : Type*} [One M] {f : α → M} {s : Set α} :
s.mulIndicator f =ᵐ[μ] 1 ↔ μ (s ∩ f.mulSupport) = 0 := by simp [EventuallyEq, eventually_iff, ae, compl_setOf]; rfl