Theorems · Theorem · measure theory
MeasurableSet.singleton
∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] (a : α), MeasurableSet {a}- Cited by
- 19 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
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
- MeasurableSetstatement · cited by 3,075
- MeasurableSingletonClassstatement and proof · cited by 230
- MeasurableSingletonClass.measurableSet_singletonproof · cited by 53
Cited by19
Results whose statement or proof uses this declaration.
- Set.Countable.measurableSetproof · cited by 14
- aemeasurable_indicator_const_iffproof · cited by 5
- measurableSet_eqproof · cited by 4
- measurable_indicator_const_iffproof · cited by 4
- Set.Subsingleton.measurableSetproof · cited by 3
- MeasurableSet.insertproof · cited by 3
- MeasurableEmbedding.prodMk_leftproof · cited by 2
- MeasureTheory.setIntegral_countableproof · cited by 2
- MeasureTheory.StronglyMeasurable.inv₀proof · cited by 2
- PMF.integral_eq_sumproof · cited by 1
- MeasureTheory.StronglyMeasurable.divproof · cited by 1
- BoundedVariationOn.vectorMeasure_singletonproof · cited by 1