Theorems · Theorem · measure theory

Set.indicator_ae_eq_zero

∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {M : Type u_4} [inst_2 : Zero M] {f : α → M} {s : Set α},
  s.indicator f =ᵐ[μ] 0 ↔ μ (s ∩ Function.support f) = 0

Defined in

Mathlib.MeasureTheory.OuterMeasure.AE

Cited by

1 results in Mathlib

Foundations

Depth 135 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FunLikeMeasureTheory.OuterMeasureClassZero