Theorems · Definition · measure theory

MeasureTheory.NullMeasurableSet

{α : Type u_2} →
  [inst : MeasurableSpace α] →
    Set α → autoParam (MeasureTheory.Measure α) MeasureTheory.NullMeasurableSet._auto_1 → Prop

A set is called NullMeasurableSet if it can be approximated by a measurable set up to a set of null measure.

Defined in: Mathlib.MeasureTheory.Measure.NullMeasurable
Cited by: 337 results in Mathlib
Foundations: Depth 173 from the axioms, rests on 4,664 definitions · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
MeasurableSetproof · cited by 3,075

Cited by343

Results whose statement or proof uses this declaration.

MeasurableSet.nullMeasurableSetstatement · cited by 155
MeasureTheory.Measure.comapproof · cited by 96
MeasureTheory.NullMeasurableproof · cited by 21
MeasureTheory.NullMeasurableSet.preimagestatement and proof · cited by 21
MeasureTheory.measure_sdiffstatement and proof · cited by 20
MeasureTheory.MeasurePreserving.measure_preimagestatement and proof · cited by 19
MeasureTheory.NullMeasurableSet.interstatement and proof · cited by 17
MeasureTheory.NullMeasurableSet.complstatement and proof · cited by 16
MeasureTheory.NullMeasurableSet.toMeasurable_ae_eqstatement and proof · cited by 13
MeasureTheory.tendsto_measure_iInter_atTopstatement and proof · cited by 12
MeasureTheory.NullMeasurableSet.mono_acstatement and proof · cited by 12
MeasureTheory.Measure.restrict_apply₀statement and proof · cited by 10

Showing the 200 most cited of 343.