Theorems · Theorem · measure theory
MeasureTheory.StronglyMeasurable.separableSpace_range_union_singleton
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x : MeasurableSpace α} [inst : TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β],
MeasureTheory.StronglyMeasurable f → ∀ {b : β}, TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {b})- Cited by
- 11 results in Mathlib
- Foundations
- Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- MeasurableSpacestatement and proof · cited by 13,106
- Set.Elemstatement · cited by 7,166
- Set.rangestatement · cited by 4,705
- MeasureTheory.StronglyMeasurablestatement and proof · cited by 363
- TopologicalSpace.PseudoMetrizableSpacestatement and proof · cited by 245
- TopologicalSpace.SeparableSpacestatement · cited by 109
- Set.finite_singletonproof · cited by 70
- MeasureTheory.StronglyMeasurable.isSeparable_rangeproof · cited by 10
- TopologicalSpace.IsSeparable.separableSpaceproof · cited by 5
- Set.Finite.isSeparableproof · cited by 4
Cited by11
Results whose statement or proof uses this declaration.
- MeasureTheory.integral_trimproof · cited by 6
- MeasureTheory.integral_mono_measureproof · cited by 5
- MeasureTheory.setToFun_of_le_map_of_stronglyMeasurableproof · cited by 2
- MeasureTheory.IntegrableOn.hasBoxIntegralproof · cited by 2
- MeasureTheory.MemLp.finStronglyMeasurable_of_stronglyMeasurableproof · cited by 2
- MeasureTheory.MemLp.exists_simpleFunc_eLpNorm_sub_ltproof · cited by 2
- MeasureTheory.Lp.simpleFunc.isDenseEmbeddingproof · cited by 1
- MeasureTheory.StronglyMeasurable.integral_kernelproof · cited by 1
- MeasureTheory.StronglyMeasurable.integral_kernel_prod_rightproof · cited by 1
- MeasureTheory.StronglyMeasurable.setToFun_prod_rightproof · cited by 1
- ProbabilityTheory.strong_law_ae_of_measurableproof · cited by 1