Theorems · Definition · measure theory
measurableAtom
{β : Type u_2} → [MeasurableSpace β] → β → Set βThe measurable atom of x is the intersection of all the measurable sets containing x.
It is measurable when the space is countable (or more generally when the measurable space is
countably generated).
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- MeasurableSpace
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
- MeasurableSetproof · cited by 3,075
- Set.iInterproof · cited by 1,084
Cited by20
Results whose statement or proof uses this declaration.
- ProbabilityTheory.Kernel.measurable_rnDerivAuxproof · cited by 8
- mem_of_mem_measurableAtomstatement and proof · cited by 4
- mem_measurableAtom_selfstatement · cited by 4
- MeasurableSet.measurableAtom_of_countablestatement and proof · cited by 3
- ProbabilityTheory.Kernel.condKernelCountablestatement and proof · cited by 3
- measurableAtom_eq_of_memstatement and proof · cited by 3
- measurable_from_prod_countable_left'statement and proof · cited by 2
- measurable_from_prod_countable_right'statement and proof · cited by 2
- measurableAtom_of_measurableSingletonClassstatement · cited by 2
- measurableAtom_subsetstatement · cited by 2
- MeasurableSpace.measurableAtom_eq_countablyGeneratedAtom_natGeneratingSequencestatement · cited by 1
- disjoint_measurableAtom_of_notMemstatement and proof · cited by 1