Theorems · Theorem · measure theory
measurable_of_tendsto_metrizable
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β] [inst_3 : MeasurableSpace β] [BorelSpace β] {f : ℕ → α → β} {g : α → β},
(∀ (i : ℕ), Measurable (f i)) → Filter.Tendsto f Filter.atTop (nhds g) → Measurable gA sequential limit of measurable functions valued in a (pseudo) metrizable space is measurable.
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 162 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- nhdsstatement and proof · cited by 5,554
- Filter.Tendstostatement and proof · cited by 3,814
- Filter.atTopstatement and proof · cited by 2,405
- BorelSpacestatement and proof · cited by 1,602
- Measurablestatement and proof · cited by 1,499
- TopologicalSpace.PseudoMetrizableSpacestatement and proof · cited by 245
- measurable_of_tendsto_metrizable'proof · cited by 7
Cited by6
Results whose statement or proof uses this declaration.
- MeasureTheory.StronglyMeasurable.measurableproof · cited by 74
- MeasureTheory.isTightMeasureSet_of_tendsto_charFunproof · cited by 1
- HasCompactSupport.measurable_of_prodproof · cited by 1
- Measurable.add_stronglyMeasurableproof · cited by 1
- Measurable.stronglyMeasurable_addproof · cited by 0
- MeasureTheory.measurable_uncurry_of_continuous_of_measurableproof · cited by 0