mulIndicator_ae_eq_one — Mathlib

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

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