Metrizable

📁 Source: Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean

Statistics

Metric	Count
Definitions	0
Theorems aemeasurable_of_tendsto_metrizable_ae, aemeasurable_of_tendsto_metrizable_ae', aemeasurable_of_unif_approx, measurableSet_of_tendsto_indicator, measurable_limit_of_tendsto_metrizable_ae, measurable_of_tendsto_metrizable, measurable_of_tendsto_metrizable', measurable_of_tendsto_metrizable_ae, nullMeasurableSet_of_tendsto_indicator	9
Total	9

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aemeasurable_of_tendsto_metrizable_ae 📖	—	AEMeasurable Filter.Eventually Filter.Tendsto nhds MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	MeasureTheory.Measure.instOuterMeasureClass Filter.exists_seq_tendsto Filter.mp_mem Filter.univ_mem' Filter.Tendsto.comp measurable_of_tendsto_metrizable' Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat instIsCountablyGenerated_atTop OrderTopology.of_linearLocallyFinite instDiscreteTopologyNat TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountableNat PseudoEMetricSpace.pseudoMetrizableSpace aeSeq.measurable tendsto_pi_nhds aeSeq.mk_eq_fun_of_mem_aeSeqSet aeSeq.fun_prop_of_mem_aeSeqSet tendsto_const_nhds Filter.EventuallyEq.symm MeasureTheory.ite_ae_eq_of_measure_compl_zero aeSeq.measure_compl_aeSeqSet_eq_zero
aemeasurable_of_tendsto_metrizable_ae' 📖	—	AEMeasurable Filter.Eventually Filter.Tendsto Filter.atTop Nat.instPreorder nhds MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	MeasureTheory.Measure.instOuterMeasureClass aemeasurable_of_tendsto_metrizable_ae Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat instIsCountablyGenerated_atTop OrderTopology.of_linearLocallyFinite instDiscreteTopologyNat TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountableNat PseudoEMetricSpace.pseudoMetrizableSpace
aemeasurable_of_unif_approx 📖	—	AEMeasurable Filter.Eventually Real Real.instLE Dist.dist PseudoMetricSpace.toDist MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	MeasureTheory.Measure.instOuterMeasureClass exists_seq_strictAnti_tendsto instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace MeasureTheory.ae_all_iff instCountableNat Filter.mp_mem Filter.univ_mem' tendsto_iff_dist_tendsto_zero squeeze_zero dist_nonneg aemeasurable_of_tendsto_metrizable_ae'
measurableSet_of_tendsto_indicator 📖	—	MeasurableSet Filter.Eventually Set Set.instMembership	—	—	measurable_indicator_const_iff instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instT2Space NeZero.charZero_one ENNReal.instCharZero ENNReal.measurable_of_tendsto' tendsto_indicator_const_iff_forall_eventually T5Space.toT1Space ENNReal.instT5Space
measurable_limit_of_tendsto_metrizable_ae 📖	mathematical	AEMeasurable Filter.Eventually Filter.Tendsto nhds MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Measurable	—	MeasureTheory.Measure.instOuterMeasureClass Filter.eq_or_neBot Filter.Eventually.of_forall Filter.tendsto_bot aeSeq.fun_prop_of_mem_aeSeqSet aeSeq.aeSeq_eq_fun_ae Filter.Tendsto.congr aeSeq.mk_eq_fun_of_mem_aeSeqSet tendsto_const_nhds Filter.Eventually.mono measurable_of_tendsto_metrizable' aeSeq.measurable tendsto_pi_nhds
measurable_of_tendsto_metrizable 📖	—	Measurable Filter.Tendsto Filter.atTop Nat.instPreorder nhds Pi.topologicalSpace	—	—	measurable_of_tendsto_metrizable' Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat instIsCountablyGenerated_atTop OrderTopology.of_linearLocallyFinite instDiscreteTopologyNat TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountableNat PseudoEMetricSpace.pseudoMetrizableSpace
measurable_of_tendsto_metrizable' 📖	—	Measurable Filter.Tendsto nhds Pi.topologicalSpace	—	—	measurable_of_isClosed' tendsto_pi_nhds Filter.Tendsto.comp Continuous.tendsto Metric.continuous_infNndist_pt NNReal.measurable_of_tendsto' Measurable.infNndist BorelSpace.opensMeasurable Set.ext IsClosed.mem_iff_infDist_zero MeasurableSingletonClass.measurableSet_singleton instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space NNReal.borelSpace NNReal.instSecondCountableTopology TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
measurable_of_tendsto_metrizable_ae 📖	—	Measurable Filter.Eventually Filter.Tendsto Filter.atTop Nat.instPreorder nhds MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	MeasureTheory.Measure.instOuterMeasureClass aemeasurable_iff_measurable aemeasurable_of_tendsto_metrizable_ae' Measurable.aemeasurable
nullMeasurableSet_of_tendsto_indicator 📖	—	MeasureTheory.NullMeasurableSet Filter.Eventually Set Set.instMembership MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	MeasureTheory.Measure.instOuterMeasureClass aemeasurable_indicator_const_iff instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instT2Space NeZero.charZero_one ENNReal.instCharZero aemeasurable_of_tendsto_metrizable_ae TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace ENNReal.instMetrizableSpace T5Space.toT1Space ENNReal.instT5Space

---

← Back to Index