Theorems · Theorem · measure theory
MeasureTheory.StronglyMeasurable.measurable
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x : MeasurableSpace α} [inst : TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : MeasurableSpace β] [BorelSpace β],
MeasureTheory.StronglyMeasurable f → Measurable fA strongly measurable function is measurable.
- Cited by
- 74 results in Mathlib
- Foundations
- Depth 163 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- MeasurableSpacestatement and proof · cited by 13,106
- BorelSpacestatement and proof · cited by 1,602
- Measurablestatement · cited by 1,499
- MeasureTheory.StronglyMeasurablestatement and proof · cited by 363
- TopologicalSpace.PseudoMetrizableSpacestatement and proof · cited by 245
- tendsto_pi_nhdsproof · cited by 58
- MeasureTheory.StronglyMeasurable.approxproof · cited by 40
- MeasureTheory.StronglyMeasurable.tendsto_approxproof · cited by 36
- MeasureTheory.SimpleFunc.measurableproof · cited by 20
- measurable_of_tendsto_metrizableproof · cited by 6
Cited by74
Results whose statement or proof uses this declaration.
- MeasureTheory.AEStronglyMeasurable.aemeasurableproof · cited by 73
- MeasureTheory.StronglyMeasurable.enormproof · cited by 19
- stronglyMeasurable_iff_measurable_separableproof · cited by 13
- stronglyMeasurable_of_tendstoproof · cited by 12
- MeasureTheory.StronglyMeasurable.measurableSet_leproof · cited by 9
- MeasureTheory.integral_trimproof · cited by 6
- MeasureTheory.StronglyAdapted.adaptedproof · cited by 5
- MeasureTheory.integral_mono_measureproof · cited by 5
- MeasureTheory.AEStronglyMeasurable.measurable_mkproof · cited by 4
- MeasureTheory.Submartingale.ae_tendsto_limitProcessproof · cited by 4
- MeasureTheory.integral_dirac'proof · cited by 4
- MeasureTheory.tendstoInMeasure_of_tendsto_aeproof · cited by 4