Theorems · Inductive type · measure theory
MeasurableSpace.CountablyGenerated
(α : Type u_3) → [m : MeasurableSpace α] → Prop
We say a measurable space is countably generated if it can be generated by a countable set of sets.
- Cited by
- 124 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- MeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement · cited by 13,106
Cited by140
Results whose statement or proof uses this declaration.
- ProbabilityTheory.Kernel.densityProcessstatement and proof · cited by 37
- MeasurableSpace.countablePartitionSetstatement and proof · cited by 24
- ProbabilityTheory.Kernel.densitystatement and proof · cited by 24
- ProbabilityTheory.countableFiltrationstatement and proof · cited by 23
- MeasurableSpace.countablePartitionstatement and proof · cited by 20
- MeasurableSpace.countable_countableGeneratingSetstatement and proof · cited by 13
- MeasurableSpace.natGeneratingSequencestatement and proof · cited by 11
- ProbabilityTheory.Kernel.measurable_rnDerivAuxproof · cited by 8
- MeasurableSpace.countableGeneratingSetstatement and proof · cited by 7
- MeasurableSpace.countablyGeneratedAtomstatement and proof · cited by 7
- MeasurableSpace.CountableOrCountablyGenerated.countableOrCountablyGeneratedstatement · cited by 6
- ProbabilityTheory.Kernel.integrable_densitystatement and proof · cited by 6