Real

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

Statistics

Metric	Count
Definitions ennrealEquivSum, ennrealEquivNNReal, erealEquivReal, finiteSpanningSetsInIooRat	4
Theorems coe_ereal_ennreal, coe_nnreal_ennreal, coe_nnreal_real, coe_real_ereal, ennreal_ofReal, ennreal_toNNReal, ennreal_toReal, ennreal_tsum, ereal_toENNReal, ereal_toReal, nnreal_tsum, real_toNNReal, aemeasurable_of_tendsto, aemeasurable_of_tendsto', instMeasurableInv, instMeasurableMul₂, instMeasurableSMulNNReal, instMeasurableSub₂, measurable_ofReal, measurable_of_measurable_nnreal, measurable_of_measurable_nnreal_nnreal, measurable_of_measurable_nnreal_prod, measurable_of_tendsto, measurable_of_tendsto', measurable_toNNReal, measurable_toReal, instMeasurableAdd₂, instMeasurableMul₂, measurableEmbedding_coe, measurable_of_measurable_real, measurable_of_real_prod, measurable_of_real_real, coe_ereal_ennreal, coe_nnreal_ennreal, coe_nnreal_real, coe_real_ereal, ennreal_ofReal, ennreal_toNNReal, ennreal_toReal, ennreal_tsum, ennreal_tsum', ereal_toENNReal, ereal_toReal, nnreal_tsum, real_toNNReal, instMeasurableSMul₂ENNReal, measurable_of_tendsto, measurable_of_tendsto', borel_eq_generateFrom_Ici_rat, borel_eq_generateFrom_Iic_rat, borel_eq_generateFrom_Iio_rat, borel_eq_generateFrom_Ioi_rat, borel_eq_generateFrom_Ioo_rat, isPiSystem_Ici_rat, isPiSystem_Iic_rat, isPiSystem_Iio_rat, isPiSystem_Ioi_rat, isPiSystem_Ioo_rat, measure_ext_Ioo_rat, aemeasurable_coe_nnreal_ennreal_iff, aemeasurable_coe_nnreal_real_iff, exists_spanning_measurableSet_le, measurable_coe_ennreal_ereal, measurable_coe_nnreal_ennreal, measurable_coe_nnreal_ennreal_iff, measurable_coe_nnreal_real, measurable_coe_nnreal_real_iff, measurable_coe_real_ereal, measurable_ereal_toENNReal, measurable_ereal_toReal, measurable_real_toNNReal, tendsto_measure_Icc, tendsto_measure_Icc_nhdsWithin_right, tendsto_measure_Icc_nhdsWithin_right'	74
Total	78

AEMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_ereal_ennreal 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	EReal EReal.measurableSpace ENNReal.toEReal	—	Measurable.comp_aemeasurable measurable_coe_ennreal_ereal
coe_nnreal_ennreal 📖	mathematical	AEMeasurable NNReal NNReal.measurableSpace	ENNReal ENNReal.measurableSpace ENNReal.ofNNReal	—	Measurable.comp_aemeasurable Continuous.measurable BorelSpace.opensMeasurable NNReal.borelSpace ENNReal.borelSpace ENNReal.continuous_coe
coe_nnreal_real 📖	mathematical	AEMeasurable NNReal NNReal.measurableSpace	Real Real.measurableSpace NNReal.toReal	—	Measurable.comp_aemeasurable measurable_coe_nnreal_real
coe_real_ereal 📖	mathematical	AEMeasurable Real Real.measurableSpace	EReal EReal.measurableSpace Real.toEReal	—	Measurable.comp_aemeasurable measurable_coe_real_ereal
ennreal_ofReal 📖	mathematical	AEMeasurable Real Real.measurableSpace	ENNReal ENNReal.measurableSpace ENNReal.ofReal	—	Measurable.comp_aemeasurable Continuous.measurable BorelSpace.opensMeasurable Real.borelSpace ENNReal.borelSpace ENNReal.continuous_ofReal
ennreal_toNNReal 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	NNReal NNReal.measurableSpace ENNReal.toNNReal	—	Measurable.comp_aemeasurable ENNReal.measurable_toNNReal
ennreal_toReal 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Real Real.measurableSpace ENNReal.toReal	—	Measurable.comp_aemeasurable ENNReal.measurable_toReal
ennreal_tsum 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	ENNReal.tsum_eq_iSup_sum iSup ENNReal.borelSpace ENNReal.instOrderTopology ENNReal.instSecondCountableTopology Finset.countable Finset.aemeasurable_fun_sum ContinuousAdd.measurableMul₂ ENNReal.instContinuousAdd
ereal_toENNReal 📖	mathematical	AEMeasurable EReal EReal.measurableSpace	ENNReal ENNReal.measurableSpace EReal.toENNReal	—	Measurable.comp_aemeasurable measurable_ereal_toENNReal
ereal_toReal 📖	mathematical	AEMeasurable EReal EReal.measurableSpace	Real Real.measurableSpace EReal.toReal	—	Measurable.comp_aemeasurable measurable_ereal_toReal
nnreal_tsum 📖	mathematical	AEMeasurable NNReal NNReal.measurableSpace	tsum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal NNReal.instTopologicalSpace SummationFilter.unconditional	—	NNReal.tsum_eq_toNNReal_tsum ennreal_toNNReal ennreal_tsum coe_nnreal_ennreal
real_toNNReal 📖	mathematical	AEMeasurable Real Real.measurableSpace	NNReal NNReal.measurableSpace Real.toNNReal	—	Measurable.comp_aemeasurable measurable_real_toNNReal

ENNReal

Definitions

Name	Category	Theorems
ennrealEquivSum 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aemeasurable_of_tendsto 📖	—	AEMeasurable ENNReal measurableSpace Filter.Eventually Filter.Tendsto Filter.atTop Nat.instPreorder nhds instTopologicalSpace MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	MeasureTheory.Measure.instOuterMeasureClass aemeasurable_of_tendsto' 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_tendsto' 📖	—	AEMeasurable ENNReal measurableSpace Filter.Eventually Filter.Tendsto nhds instTopologicalSpace 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' 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
instMeasurableInv 📖	mathematical	—	MeasurableInv ENNReal instInv measurableSpace	—	Continuous.measurable BorelSpace.opensMeasurable borelSpace ContinuousInv.continuous_inv instContinuousInv
instMeasurableMul₂ 📖	mathematical	—	MeasurableMul₂ ENNReal measurableSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring	—	measurable_of_measurable_nnreal_nnreal Measurable.coe_nnreal_ennreal MeasurableMul₂.measurable_mul ContinuousMul.measurableMul₂ NNReal.borelSpace NNReal.instSecondCountableTopology IsTopologicalSemiring.toContinuousMul NNReal.instIsTopologicalSemiring top_mul' Measurable.piecewise MeasurableSingletonClass.measurableSet_singleton instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace measurable_const mul_top'
instMeasurableSMulNNReal 📖	mathematical	—	MeasurableSMul NNReal ENNReal Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring instCommSemiring instAlgebraNNReal Algebra.id NNReal.measurableSpace measurableSpace	—	MeasurableConstSMul.measurable_const_smul MeasurableSMul.toMeasurableConstSMul measurableSMul_of_mul MeasurableMul₂.toMeasurableMul instMeasurableMul₂ Measurable.mul_const measurable_coe_nnreal_ennreal
instMeasurableSub₂ 📖	mathematical	—	MeasurableSub₂ ENNReal measurableSpace instSub	—	measurable_of_measurable_nnreal_nnreal Measurable.coe_nnreal_ennreal MeasurableSub₂.measurable_sub ContinuousSub.measurableSub₂ NNReal.borelSpace NNReal.instSecondCountableTopology NNReal.instContinuousSub top_sub sub_top
measurable_ofReal 📖	mathematical	—	Measurable Real ENNReal Real.measurableSpace measurableSpace ofReal	—	Continuous.measurable BorelSpace.opensMeasurable Real.borelSpace borelSpace continuous_ofReal
measurable_of_measurable_nnreal 📖	mathematical	Measurable NNReal NNReal.measurableSpace ofNNReal	ENNReal measurableSpace	—	measurable_of_measurable_on_compl_singleton instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable borelSpace instSecondCountableTopology instT2Space MeasurableEquiv.measurable_comp_iff
measurable_of_measurable_nnreal_nnreal 📖	mathematical	Measurable NNReal Prod.instMeasurableSpace NNReal.measurableSpace ENNReal ofNNReal Top.top instTopENNReal	measurableSpace	—	measurable_of_measurable_nnreal_prod measurable_swap_iff Measurable.comp measurable_swap measurable_of_measurable_nnreal
measurable_of_measurable_nnreal_prod 📖	mathematical	Measurable NNReal Prod.instMeasurableSpace NNReal.measurableSpace ENNReal ofNNReal Top.top instTopENNReal	measurableSpace	—	MeasurableEquiv.measurable_comp_iff measurable_fun_sum Measurable.comp Measurable.snd measurable_id
measurable_of_tendsto 📖	—	Measurable ENNReal measurableSpace Filter.Tendsto Filter.atTop Nat.instPreorder nhds Pi.topologicalSpace instTopologicalSpace	—	—	measurable_of_tendsto' 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' 📖	—	Measurable ENNReal measurableSpace Filter.Tendsto nhds Pi.topologicalSpace instTopologicalSpace	—	—	Filter.exists_seq_tendsto Filter.Tendsto.liminf_eq instOrderTopology Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Tendsto.comp tendsto_pi_nhds Measurable.liminf borelSpace instSecondCountableTopology
measurable_toNNReal 📖	mathematical	—	Measurable ENNReal NNReal measurableSpace NNReal.measurableSpace toNNReal	—	measurable_of_measurable_nnreal measurable_id
measurable_toReal 📖	mathematical	—	Measurable ENNReal Real measurableSpace Real.measurableSpace toReal	—	measurable_of_measurable_nnreal measurable_coe_nnreal_real

EReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMeasurableAdd₂ 📖	mathematical	—	MeasurableAdd₂ EReal measurableSpace AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommMonoidEReal	—	LowerSemicontinuous.measurable borelSpace instOrderTopology instSecondCountableTopology Prod.opensMeasurableSpace BorelSpace.opensMeasurable secondCountableTopologyEither_of_right lowerSemicontinuous_add
instMeasurableMul₂ 📖	mathematical	—	MeasurableMul₂ EReal measurableSpace instMul	—	measurable_of_real_real Measurable.coe_real_ereal Measurable.mul ContinuousMul.measurableMul₂ Real.borelSpace instSecondCountableTopologyReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal measurable_fst measurable_snd Measurable.comp measurable_coe_real_ereal mul_comm
measurableEmbedding_coe 📖	mathematical	—	MeasurableEmbedding Real EReal Real.measurableSpace measurableSpace Real.toEReal	—	Topology.IsOpenEmbedding.measurableEmbedding Real.borelSpace borelSpace isOpenEmbedding_coe
measurable_of_measurable_real 📖	mathematical	Measurable Real Real.measurableSpace Real.toEReal	EReal measurableSpace	—	measurable_of_measurable_on_compl_finite instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable borelSpace instSecondCountableTopology instT2Space MeasurableEquiv.measurable_comp_iff
measurable_of_real_prod 📖	mathematical	Measurable Real Prod.instMeasurableSpace Real.measurableSpace EReal Real.toEReal Bot.bot instBotEReal Top.top instTop	measurableSpace	—	Measurable.of_union₃_range_cover measurableEmbedding_prodMk_left instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable borelSpace instSecondCountableTopology instT2Space MeasurableEmbedding.prodMap measurableEmbedding_coe MeasurableEmbedding.id Set.range_prodMap Set.range_id
measurable_of_real_real 📖	mathematical	Measurable Real Prod.instMeasurableSpace Real.measurableSpace EReal Real.toEReal Bot.bot instBotEReal Top.top instTop	measurableSpace	—	measurable_of_real_prod measurable_swap_iff Measurable.comp measurable_swap measurable_of_measurable_real

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_ereal_ennreal 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	EReal EReal.measurableSpace ENNReal.toEReal	—	comp measurable_coe_ennreal_ereal
coe_nnreal_ennreal 📖	mathematical	Measurable NNReal NNReal.measurableSpace	ENNReal ENNReal.measurableSpace ENNReal.ofNNReal	—	comp Continuous.measurable BorelSpace.opensMeasurable NNReal.borelSpace ENNReal.borelSpace ENNReal.continuous_coe
coe_nnreal_real 📖	mathematical	Measurable NNReal NNReal.measurableSpace	Real Real.measurableSpace NNReal.toReal	—	comp measurable_coe_nnreal_real
coe_real_ereal 📖	mathematical	Measurable Real Real.measurableSpace	EReal EReal.measurableSpace Real.toEReal	—	comp measurable_coe_real_ereal
ennreal_ofReal 📖	mathematical	Measurable Real Real.measurableSpace	ENNReal ENNReal.measurableSpace ENNReal.ofReal	—	comp Continuous.measurable BorelSpace.opensMeasurable Real.borelSpace ENNReal.borelSpace ENNReal.continuous_ofReal
ennreal_toNNReal 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	NNReal NNReal.measurableSpace ENNReal.toNNReal	—	comp ENNReal.measurable_toNNReal
ennreal_toReal 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	Real Real.measurableSpace ENNReal.toReal	—	comp ENNReal.measurable_toReal
ennreal_tsum 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	ENNReal.tsum_eq_iSup_sum iSup ENNReal.borelSpace ENNReal.instOrderTopology ENNReal.instSecondCountableTopology Finset.countable Finset.measurable_fun_sum ContinuousAdd.measurableMul₂ ENNReal.instContinuousAdd
ennreal_tsum' 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	tsum Pi.addCommMonoid ENNReal.instAddCommMonoid Pi.topologicalSpace ENNReal.instTopologicalSpace SummationFilter.unconditional	—	tsum_apply SummationFilter.instNeBotUnconditional ENNReal.instT2Space Pi.summable ENNReal.summable ennreal_tsum
ereal_toENNReal 📖	mathematical	Measurable EReal EReal.measurableSpace	ENNReal ENNReal.measurableSpace EReal.toENNReal	—	comp measurable_ereal_toENNReal
ereal_toReal 📖	mathematical	Measurable EReal EReal.measurableSpace	Real Real.measurableSpace EReal.toReal	—	comp measurable_ereal_toReal
nnreal_tsum 📖	mathematical	Measurable NNReal NNReal.measurableSpace	tsum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal NNReal.instTopologicalSpace SummationFilter.unconditional	—	NNReal.tsum_eq_toNNReal_tsum ennreal_toNNReal ennreal_tsum coe_nnreal_ennreal
real_toNNReal 📖	mathematical	Measurable Real Real.measurableSpace	NNReal NNReal.measurableSpace Real.toNNReal	—	comp measurable_real_toNNReal

MeasurableEquiv

Definitions

Name	Category	Theorems
ennrealEquivNNReal 📖	CompOp	—
erealEquivReal 📖	CompOp	—

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMeasurableSMul₂ENNReal 📖	mathematical	—	MeasurableSMul₂ NNReal ENNReal Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id measurableSpace ENNReal.measurableSpace	—	Measurable.mul ENNReal.instMeasurableMul₂ Measurable.coe_nnreal_ennreal Measurable.fst measurable_id' Measurable.snd
measurable_of_tendsto 📖	—	Measurable NNReal measurableSpace Filter.Tendsto Filter.atTop Nat.instPreorder nhds Pi.topologicalSpace instTopologicalSpace	—	—	measurable_of_tendsto' 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' 📖	—	Measurable NNReal measurableSpace Filter.Tendsto nhds Pi.topologicalSpace instTopologicalSpace	—	—	ENNReal.measurable_of_tendsto' tendsto_pi_nhds Filter.Tendsto.comp Continuous.tendsto ENNReal.continuous_coe

Real

Definitions

Name	Category	Theorems
finiteSpanningSetsInIooRat 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borel_eq_generateFrom_Ici_rat 📖	mathematical	—	borel Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace MeasurableSpace.generateFrom Set.iUnion Set Set.instSingletonSet Set.Ici instPreorder instRatCast	—	borel_eq_generateFrom_Iio_rat Set.iUnion_singleton_eq_range le_antisymm MeasurableSpace.generateFrom_le Set.compl_Ici MeasurableSet.compl Set.mem_range_self Set.compl_Iio
borel_eq_generateFrom_Iic_rat 📖	mathematical	—	borel Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace MeasurableSpace.generateFrom Set.iUnion Set Set.instSingletonSet Set.Iic instPreorder instRatCast	—	borel_eq_generateFrom_Ioi_rat Set.iUnion_singleton_eq_range le_antisymm MeasurableSpace.generateFrom_le Set.compl_Iic MeasurableSet.compl Set.mem_range_self Set.compl_Ioi
borel_eq_generateFrom_Iio_rat 📖	mathematical	—	borel Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace MeasurableSpace.generateFrom Set.iUnion Set Set.instSingletonSet Set.Iio instPreorder instRatCast	—	borel_eq_generateFrom_Iio instSecondCountableTopologyReal instOrderTopologyReal le_antisymm MeasurableSpace.generateFrom_le instIsStrictOrderedRing instArchimedean IsLUB.biUnion_Iio_eq Set.image_univ Set.image_inter_preimage Set.univ_inter Set.biUnion_image MeasurableSet.biUnion Set.to_countable SetCoe.countable Encodable.countable Set.iUnion_singleton_eq_range MeasurableSpace.generateFrom_mono Set.iUnion_subset Set.singleton_subset_iff Set.mem_range_self
borel_eq_generateFrom_Ioi_rat 📖	mathematical	—	borel Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace MeasurableSpace.generateFrom Set.iUnion Set Set.instSingletonSet Set.Ioi instPreorder instRatCast	—	borel_eq_generateFrom_Ioi instSecondCountableTopologyReal instOrderTopologyReal le_antisymm MeasurableSpace.generateFrom_le instIsStrictOrderedRing instArchimedean IsGLB.biUnion_Ioi_eq Set.image_univ Set.image_inter_preimage Set.univ_inter Set.biUnion_image MeasurableSet.biUnion Set.to_countable SetCoe.countable Encodable.countable Set.iUnion_singleton_eq_range MeasurableSpace.generateFrom_mono Set.iUnion_subset Set.singleton_subset_iff Set.mem_range_self
borel_eq_generateFrom_Ioo_rat 📖	mathematical	—	borel Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace MeasurableSpace.generateFrom Set.iUnion Set Set.instSingletonSet Set.Ioo instPreorder instRatCast	—	TopologicalSpace.IsTopologicalBasis.borel_eq_generateFrom instSecondCountableTopologyReal isTopologicalBasis_Ioo_rat
isPiSystem_Ici_rat 📖	mathematical	—	IsPiSystem Real Set.iUnion Set Set.instSingletonSet Set.Ici instPreorder instRatCast	—	Set.ext Set.iUnion_singleton_eq_range Set.image_univ isPiSystem_image_Ici
isPiSystem_Iic_rat 📖	mathematical	—	IsPiSystem Real Set.iUnion Set Set.instSingletonSet Set.Iic instPreorder instRatCast	—	Set.ext Set.iUnion_singleton_eq_range Set.image_univ isPiSystem_image_Iic
isPiSystem_Iio_rat 📖	mathematical	—	IsPiSystem Real Set.iUnion Set Set.instSingletonSet Set.Iio instPreorder instRatCast	—	Set.ext Set.iUnion_singleton_eq_range Set.image_univ isPiSystem_image_Iio
isPiSystem_Ioi_rat 📖	mathematical	—	IsPiSystem Real Set.iUnion Set Set.instSingletonSet Set.Ioi instPreorder instRatCast	—	Set.ext Set.iUnion_singleton_eq_range Set.image_univ isPiSystem_image_Ioi
isPiSystem_Ioo_rat 📖	mathematical	—	IsPiSystem Real Set.iUnion Set Set.instSingletonSet Set.Ioo instPreorder instRatCast	—	Set.ext instIsStrictOrderedRing isPiSystem_Ioo
measure_ext_Ioo_rat 📖	—	DFunLike.coe MeasureTheory.Measure Real measurableSpace Set ENNReal MeasureTheory.Measure.instFunLike Set.Ioo instPreorder instRatCast	—	—	MeasureTheory.Measure.FiniteSpanningSetsIn.ext borel_eq_generateFrom_Ioo_rat isPiSystem_Ioo_rat

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aemeasurable_coe_nnreal_ennreal_iff 📖	mathematical	—	AEMeasurable ENNReal ENNReal.measurableSpace ENNReal.ofNNReal NNReal NNReal.measurableSpace	—	AEMeasurable.ennreal_toNNReal AEMeasurable.coe_nnreal_ennreal
aemeasurable_coe_nnreal_real_iff 📖	mathematical	—	AEMeasurable Real Real.measurableSpace NNReal.toReal NNReal NNReal.measurableSpace	—	Real.toNNReal_coe AEMeasurable.real_toNNReal AEMeasurable.coe_nnreal_real
exists_spanning_measurableSet_le 📖	mathematical	Measurable NNReal NNReal.measurableSpace	MeasurableSet ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Top.top instTopENNReal Preorder.toLE instPartialOrderNNReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal Set.iUnion Set.univ	—	Set.ext exists_nat_ge NNReal.instIsOrderedRing NNReal.instArchimedean MeasurableSet.inter MeasureTheory.measurableSet_spanningSets measurableSet_Iic BorelSpace.opensMeasurable NNReal.borelSpace instClosedIicTopology OrderTopology.to_orderClosedTopology NNReal.instOrderTopology LE.le.trans_lt MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass Set.inter_subset_left MeasureTheory.measure_spanningSets_lt_top Set.iUnion_inter_of_monotone instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat MeasureTheory.monotone_spanningSets LE.le.trans NNReal.addLeftMono IsStrictOrderedRing.toZeroLEOneClass NNReal.instIsStrictOrderedRing IsStrictOrderedRing.toCharZero MeasureTheory.iUnion_spanningSets Set.inter_univ
measurable_coe_ennreal_ereal 📖	mathematical	—	Measurable ENNReal EReal ENNReal.measurableSpace EReal.measurableSpace ENNReal.toEReal	—	Continuous.measurable BorelSpace.opensMeasurable ENNReal.borelSpace EReal.borelSpace continuous_coe_ennreal_ereal
measurable_coe_nnreal_ennreal 📖	mathematical	—	Measurable NNReal ENNReal NNReal.measurableSpace ENNReal.measurableSpace ENNReal.ofNNReal	—	Continuous.measurable BorelSpace.opensMeasurable NNReal.borelSpace ENNReal.borelSpace ENNReal.continuous_coe
measurable_coe_nnreal_ennreal_iff 📖	mathematical	—	Measurable ENNReal ENNReal.measurableSpace ENNReal.ofNNReal NNReal NNReal.measurableSpace	—	Measurable.ennreal_toNNReal Measurable.coe_nnreal_ennreal
measurable_coe_nnreal_real 📖	mathematical	—	Measurable NNReal Real NNReal.measurableSpace Real.measurableSpace NNReal.toReal	—	Continuous.measurable BorelSpace.opensMeasurable NNReal.borelSpace Real.borelSpace NNReal.continuous_coe
measurable_coe_nnreal_real_iff 📖	mathematical	—	Measurable Real Real.measurableSpace NNReal.toReal NNReal NNReal.measurableSpace	—	Real.toNNReal_coe Measurable.real_toNNReal Measurable.coe_nnreal_real
measurable_coe_real_ereal 📖	mathematical	—	Measurable Real EReal Real.measurableSpace EReal.measurableSpace Real.toEReal	—	Continuous.measurable BorelSpace.opensMeasurable Real.borelSpace EReal.borelSpace continuous_coe_real_ereal
measurable_ereal_toENNReal 📖	mathematical	—	Measurable EReal ENNReal EReal.measurableSpace ENNReal.measurableSpace EReal.toENNReal	—	EReal.measurable_of_measurable_real EReal.toENNReal_of_ne_top ENNReal.measurable_ofReal
measurable_ereal_toReal 📖	mathematical	—	Measurable EReal Real EReal.measurableSpace Real.measurableSpace EReal.toReal	—	EReal.measurable_of_measurable_real measurable_id
measurable_real_toNNReal 📖	mathematical	—	Measurable Real NNReal Real.measurableSpace NNReal.measurableSpace Real.toNNReal	—	Continuous.measurable BorelSpace.opensMeasurable Real.borelSpace NNReal.borelSpace continuous_real_toNNReal
tendsto_measure_Icc 📖	mathematical	—	Filter.Tendsto Real ENNReal DFunLike.coe MeasureTheory.Measure Real.measurableSpace Set MeasureTheory.Measure.instFunLike Set.Icc Real.instPreorder Real.instSub Real.instAdd nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero ENNReal.instTopologicalSpace instZeroENNReal	—	nhdsLT_sup_nhdsGE Filter.tendsto_sup Filter.Tendsto.congr' tendsto_const_nhds Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' Set.Icc_eq_empty Mathlib.Tactic.Linarith.lt_irrefl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true IsStrictOrderedRing.toCharZero Mathlib.Tactic.Linarith.sub_nonpos_of_le MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.NoAtoms.measure_singleton tendsto_measure_Icc_nhdsWithin_right
tendsto_measure_Icc_nhdsWithin_right 📖	mathematical	—	Filter.Tendsto Real ENNReal DFunLike.coe MeasureTheory.Measure Real.measurableSpace Set MeasureTheory.Measure.instFunLike Set.Icc Real.instPreorder Real.instSub Real.instAdd nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Set.Ici nhds ENNReal.instTopologicalSpace Set.instSingletonSet	—	nhdsWithin_singleton tendsto_measure_Icc_nhdsWithin_right' sub_zero add_zero Set.Icc_self mem_of_mem_nhds
tendsto_measure_Icc_nhdsWithin_right' 📖	mathematical	—	Filter.Tendsto Real ENNReal DFunLike.coe MeasureTheory.Measure Real.measurableSpace Set MeasureTheory.Measure.instFunLike Set.Icc Real.instPreorder Real.instSub Real.instAdd nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Set.Ioi nhds ENNReal.instTopologicalSpace Set.instSingletonSet	—	Real.singleton_eq_inter_Icc MeasureTheory.tendsto_measure_biInter_gt instOrderTopologyReal TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace nullMeasurableSet_Icc BorelSpace.opensMeasurable Real.borelSpace OrderTopology.to_orderClosedTopology Set.Icc_subset_Icc le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero IsCompact.measure_ne_top CompactIccSpace.isCompact_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace

---

← Back to Index