Theorems · Theorem · measure theory

interior_ae_eq_of_null_frontier

∀ {α' : Type u_6} [inst : TopologicalSpace α'] [inst_1 : MeasurableSpace α'] {μ : MeasureTheory.Measure α'}
  {s : Set α'}, μ (frontier s) = 0 → interior s =ᵐ[μ] s

Defined in

Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpace