Theorems · Theorem · measure theory

MeasureTheory.exists_null_frontier_thickening

∀ {Ω : Type u_1} [inst : PseudoMetricSpace Ω] [inst_1 : MeasurableSpace Ω] [OpensMeasurableSpace Ω]
  (μ : MeasureTheory.Measure Ω) [MeasureTheory.SFinite μ] (s : Set Ω) {a b : ℝ},
  a < b → ∃ r ∈ Set.Ioo a b, μ (frontier (Metric.thickening r s)) = 0

Defined in

Mathlib.MeasureTheory.Measure.Portmanteau

Cited by

3 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceMeasurableSpaceOpensMeasurableSpaceMeasureTheory.SFinite