Theorems · Theorem · measure theory

IsUnifLocDoublingMeasure.vitaliFamily_def

∀ {α : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
  [inst_2 : IsUnifLocDoublingMeasure μ] [inst_3 : SecondCountableTopology α] [inst_4 : BorelSpace α]
  [inst_5 : MeasureTheory.IsLocallyFiniteMeasure μ] (K : ℝ),
  IsUnifLocDoublingMeasure.vitaliFamily μ K =
    let R := IsUnifLocDoublingMeasure.scalingScaleOf μ (max (4 * K + 3) 3);
    have Rpos := ⋯;
    have A := ⋯;
    (Vitali.vitaliFamily μ (IsUnifLocDoublingMeasure.scalingConstantOf μ (max (4 * K + 3) 3)) A).enlarge (R / 4) ⋯

Defined in

Mathlib.MeasureTheory.Covering.DensityTheorem

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceMeasurableSpaceIsUnifLocDoublingMeasureSecondCountableTopologyBorelSpaceMeasureTheory.IsLocallyFiniteMeasure