Theorems · Inductive type · measure theory
MeasurableSpace.CountableOrCountablyGenerated
Type u_5 → (β : Type u_6) → [MeasurableSpace β] → Prop
A class registering that either α is countable or β is a countably generated
measurable space.
- Cited by
- 97 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 by105
Results whose statement or proof uses this declaration.
- ProbabilityTheory.Kernel.rnDerivstatement · cited by 45
- ProbabilityTheory.Kernel.rnDerivAuxstatement and proof · cited by 22
- ProbabilityTheory.Kernel.mutuallySingularSetSlicestatement and proof · cited by 19
- ProbabilityTheory.Kernel.singularPartstatement · cited by 17
- ProbabilityTheory.Kernel.condKernelstatement · cited by 16
- ProbabilityTheory.Kernel.rnDeriv_eq_rnDeriv_measurestatement and proof · cited by 13
- ProbabilityTheory.Kernel.measurable_rnDerivstatement and proof · cited by 11
- ProbabilityTheory.Kernel.measurable_rnDerivAuxstatement and proof · cited by 8
- ProbabilityTheory.Kernel.rnDeriv_add_singularPartstatement and proof · cited by 7
- MeasurableSpace.CountableOrCountablyGenerated.countableOrCountablyGeneratedstatement and proof · cited by 6
- ProbabilityTheory.Kernel.measurableSet_mutuallySingularSetSlicestatement and proof · cited by 6
- ProbabilityTheory.Kernel.mutuallySingular_singularPartstatement and proof · cited by 6