Theorems · Definition · measure theory
VitaliFamily.setsAt
{X : Type u_1} →
[inst : PseudoMetricSpace X] →
{m : MeasurableSpace X} → {μ : MeasureTheory.Measure X} → VitaliFamily μ → X → Set (Set X)Sets of the family "centered" at a given point.
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
- Assumes
- PseudoMetricSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- PseudoMetricSpacestatement and proof · cited by 1,550
- VitaliFamilystatement and proof · cited by 68
Cited by26
Results whose statement or proof uses this declaration.
- VitaliFamily.filterAtproof · cited by 49
- VitaliFamily.FineSubfamilyOnproof · cited by 18
- VitaliFamily.FineSubfamilyOn.exists_disjoint_covering_aestatement and proof · cited by 5
- VitaliFamily.measure_le_of_frequently_leproof · cited by 5
- VitaliFamily.tendsto_filterAt_iffstatement and proof · cited by 5
- Besicovitch.tendsto_filterAtproof · cited by 4
- VitaliFamily.eventually_filterAt_measurableSetproof · cited by 4
- IsUnifLocDoublingMeasure.closedBall_mem_vitaliFamily_of_dist_le_mulstatement and proof · cited by 3
- VitaliFamily.ae_eventually_measure_posproof · cited by 3
- VitaliFamily.filterAt_basis_closedBallstatement · cited by 2
- VitaliFamily.FineSubfamilyOn.covering_mem_familystatement · cited by 2
- VitaliFamily.measurableSetstatement · cited by 2