Stieltjes

📁 Source: Mathlib/MeasureTheory/Measure/Stieltjes.lean

Statistics

Metric	Count
Definitions Iotop, stieltjesFunction, StieltjesFunction, add, const, id, instAddCommMonoid, instAddZeroClass, instCoeFun, instInhabited, instModuleNNReal, length, measure, outer, toFun, botSet	16
Theorems Ioc_diff_botSet, Ioo_subset_Iotop, Iotop_subset_Ioc, stieltjesFunction_eq, add_apply, borel_le_measurable, const_apply, countable_leftLim_ne, eq_of_measure_of_eq, eq_of_measure_of_tendsto_atBot, ext, ext_iff, iInf_Ioi_eq, iInf_rat_gt_eq, id_apply, id_leftLim, instIsLocallyFiniteMeasure, isFiniteMeasure, isFiniteMeasure_of_forall_abs_le, isProbabilityMeasure, length_Ioc, length_diff_botSet, length_empty, length_eq, length_eq_of_isEmpty, length_mono, length_subadditive_Icc_Ioo, measurableSet_Ioi, measure_Icc, measure_Ici, measure_Ici_of_tendsto_atTop_atTop, measure_Ico, measure_Iic, measure_Iic_of_tendsto_atBot_atBot, measure_Iio, measure_Iio_of_tendsto_atBot_atBot, measure_Ioc, measure_Ioi, measure_Ioi_of_tendsto_atTop_atTop, measure_Ioo, measure_add, measure_botSet, measure_const, measure_def, measure_singleton, measure_smul, measure_univ, measure_univ_of_tendsto_atBot_atBot, measure_univ_of_tendsto_atTop_atTop, measure_zero, mono, mono', outer_Ioc, outer_le_length, outer_trim, rightLim_eq, right_continuous, right_continuous', zero_apply, botSet_eq_singleton_of_isBot, isOpen_Iotop, measurableSet_botSet, notMem_botSet_of_lt, subsingleton_botSet	64
Total	80

Monotone

Definitions

Name	Category	Theorems
stieltjesFunction 📖	CompOp	2 math math: ae_hasDerivAt, stieltjesFunction_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
stieltjesFunction_eq 📖	mathematical	Monotone Real PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Real.instPreorder	StieltjesFunction.toFun stieltjesFunction Function.rightLim Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	—

StieltjesFunction

Definitions

Name	Category	Theorems
add 📖	CompOp	—
const 📖	CompOp	2 math math: const_apply, measure_const
id 📖	CompOp	4 math math: Real.volume_val, id_leftLim, Real.volume_eq_stieltjes_id, id_apply
instAddCommMonoid 📖	CompOp	3 math math: add_apply, measure_add, measure_smul
instAddZeroClass 📖	CompOp	3 math math: measure_zero, zero_apply, measure_smul
instCoeFun 📖	CompOp	—
instInhabited 📖	CompOp	—
instModuleNNReal 📖	CompOp	1 math math: measure_smul
length 📖	CompOp	7 math math: length_diff_botSet, length_eq_of_isEmpty, length_empty, length_eq, outer_le_length, length_mono, length_Ioc
measure 📖	CompOp	47 math math: ProbabilityTheory.cdf_measure_stieltjesFunction, measure_univ_of_tendsto_atBot_atBot, measure_botSet, measure_zero, measure_Ioi_of_tendsto_atTop_atTop, measure_Ici_of_tendsto_atTop_atTop, measure_Ioo, Real.volume_val, instIsLocallyFiniteMeasure, measure_singleton, measure_univ, ProbabilityTheory.IsMeasurableRatCDF.instIsProbabilityMeasure_stieltjesFunction, Real.volume_eq_stieltjes_id, measure_Iic_of_tendsto_atBot_atBot, measure_univ_of_tendsto_atTop_atTop, ProbabilityTheory.IsMeasurableRatCDF.measure_stieltjesFunction_univ, Monotone.ae_hasDerivAt, measurable_measure, isFiniteMeasure_of_forall_abs_le, measure_Ici, ProbabilityTheory.measurable_measure_stieltjesOfMeasurableRat, isProbabilityMeasure, measure_Ioi, ProbabilityTheory.instIsProbabilityMeasureCondCDF, ProbabilityTheory.measure_cdf, ProbabilityTheory.IsMeasurableRatCDF.measure_stieltjesFunction_Iic, ProbabilityTheory.measure_stieltjesOfMeasurableRat_univ, measure_Icc, measure_def, isFiniteMeasure, ProbabilityTheory.measure_stieltjesOfMeasurableRat_Iic, measure_add, measure_Ioc, measure_Iio, measure_smul, ae_hasDerivAt, ProbabilityTheory.measure_condCDF_Iic, ProbabilityTheory.measurable_measure_condCDF, ProbabilityTheory.instIsProbabilityMeasure_stieltjesOfMeasurableRat, ProbabilityTheory.IsMeasurableRatCDF.measurable_measure_stieltjesFunction, ProbabilityTheory.measure_condCDF_univ, measure_Ico, measure_Iic, measure_Iio_of_tendsto_atBot_atBot, ProbabilityTheory.IsCondKernelCDF.toKernel_apply, ProbabilityTheory.instIsProbabilityMeasurecdf, measure_const
outer 📖	CompOp	5 math math: borel_le_measurable, measurableSet_Ioi, outer_le_length, outer_Ioc, outer_trim
toFun 📖	CompOp	94 math math: ProbabilityTheory.stieltjesOfMeasurableRat_ae_eq, ProbabilityTheory.condCDF_ae_eq, ProbabilityTheory.lintegral_condCDF, ProbabilityTheory.condCDF_nonneg, ProbabilityTheory.IsCondKernelCDF.toKernel_Iic, ProbabilityTheory.IsCondKernelCDF.le_one, rightLim_eq, ProbabilityTheory.unitInterval.cdf_eq_real, ProbabilityTheory.tendsto_condCDF_atBot, ProbabilityTheory.setIntegral_condCDF, ProbabilityTheory.IsCondKernelCDF.tendsto_atTop_one, measure_Ioo, ProbabilityTheory.cdf_paretoMeasure_eq_integral, ProbabilityTheory.setLIntegral_stieltjesOfMeasurableRat_rat, ProbabilityTheory.IsCondKernelCDF.nonneg, ProbabilityTheory.cdf_expMeasure_eq, ProbabilityTheory.IsCondKernelCDF.integral, mono', ProbabilityTheory.stieltjesOfMeasurableRat_nonneg, ProbabilityTheory.monotone_cdf, measure_singleton, ProbabilityTheory.integral_stieltjesOfMeasurableRat, ProbabilityTheory.integrable_condCDF, ProbabilityTheory.tendsto_stieltjesOfMeasurableRat_atTop, const_apply, ProbabilityTheory.stieltjesOfMeasurableRat_le_one, id_leftLim, ProbabilityTheory.cdf_eq_real, ProbabilityTheory.cdf_nonneg, iInf_rat_gt_eq, ProbabilityTheory.IsMeasurableRatCDF.stronglyMeasurable_stieltjesFunction, ProbabilityTheory.ofReal_condCDF_ae_eq, ProbabilityTheory.IsCondKernelCDF.setIntegral, length_subadditive_Icc_Ioo, ProbabilityTheory.IsCondKernelCDF.setLIntegral, ProbabilityTheory.cdf_le_one, countable_leftLim_ne, ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat, ProbabilityTheory.cdf_gammaMeasure_eq_lintegral, measure_Ici, zero_apply, add_apply, ProbabilityTheory.stronglyMeasurable_stieltjesOfMeasurableRat, mono, measure_Ioi, ProbabilityTheory.IsCondKernelCDF.measurable, ProbabilityTheory.tendsto_stieltjesOfMeasurableRat_atBot, BoundedVariationOn.stieltjesFunctionRightLim_apply, ProbabilityTheory.measurable_stieltjesOfMeasurableRat, ProbabilityTheory.stieltjesOfMeasurableRat_eq, ProbabilityTheory.cdf_expMeasure_eq_integral, ProbabilityTheory.IsCondKernelCDF.integrable, ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction_eq, ProbabilityTheory.IsMeasurableRatCDF.measure_stieltjesFunction_Iic, ProbabilityTheory.IsCondKernelCDF.tendsto_atBot_zero, ext_iff, measure_Icc, ProbabilityTheory.IsMeasurableRatCDF.measurable_stieltjesFunction, length_eq, ProbabilityTheory.integral_condCDF, ProbabilityTheory.condCDF_le_one, ProbabilityTheory.measure_stieltjesOfMeasurableRat_Iic, ProbabilityTheory.tendsto_cdf_atTop, measure_Ioc, ProbabilityTheory.cdf_expMeasure_eq_lintegral, ProbabilityTheory.stronglyMeasurable_condCDF, iInf_Ioi_eq, measure_Iio, ae_hasDerivAt, ProbabilityTheory.measure_condCDF_Iic, id_apply, outer_Ioc, ProbabilityTheory.setLIntegral_condCDF, ProbabilityTheory.lintegral_stieltjesOfMeasurableRat, measure_Ico, ProbabilityTheory.measurable_condCDF, ProbabilityTheory.IsMeasurableRatCDF.tendsto_stieltjesFunction_atTop, ProbabilityTheory.IsCondKernelCDF.lintegral, length_Ioc, measure_Iic, ProbabilityTheory.cdf_paretoMeasure_eq_lintegral, ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat_rat, ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction_le_one, Monotone.stieltjesFunction_eq, ProbabilityTheory.setLIntegral_stieltjesOfMeasurableRat, right_continuous, ProbabilityTheory.tendsto_cdf_atBot, ProbabilityTheory.tendsto_condCDF_atTop, ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction_nonneg, ProbabilityTheory.cdf_gammaMeasure_eq_integral, ProbabilityTheory.ofReal_cdf, ProbabilityTheory.IsMeasurableRatCDF.tendsto_stieltjesFunction_atBot, ProbabilityTheory.integrable_stieltjesOfMeasurableRat, right_continuous'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	toFun StieltjesFunction AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommMonoid Real Real.instAdd	—	—
borel_le_measurable 📖	mathematical	—	MeasurableSpace MeasurableSpace.instLE borel MeasureTheory.OuterMeasure.caratheodory outer	—	borel_eq_generateFrom_Ioi MeasurableSpace.generateFrom_le measurableSet_Ioi
const_apply 📖	mathematical	—	toFun const	—	—
countable_leftLim_ne 📖	mathematical	—	Set.Countable setOf Real Function.leftLim UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace toFun	—	Set.Countable.mono Monotone.continuousWithinAt_Iio_iff_leftLim_eq instOrderTopologyReal mono ContinuousAt.continuousWithinAt Monotone.countable_not_continuousAt instSecondCountableTopologyReal
eq_of_measure_of_eq 📖	—	measure toFun	—	—	ext le_total measure_Ioc ENNReal.ofReal_eq_ofReal_iff sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mono
eq_of_measure_of_tendsto_atBot 📖	—	measure Filter.Tendsto Real toFun Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	—	ext measure_Iic ENNReal.ofReal_eq_ofReal_iff sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Monotone.le_of_tendsto OrderTopology.to_orderClosedTopology instOrderTopologyReal SemilatticeInf.instIsCodirectedOrder mono
ext 📖	—	toFun	—	—	mono' right_continuous'
ext_iff 📖	mathematical	—	toFun	—	ext
iInf_Ioi_eq 📖	mathematical	—	iInf Real Set.Elem Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Real.instInfSet toFun Set Set.instMembership	—	Monotone.rightLim_eq_sInf instOrderTopologyReal mono Filter.neBot_iff nhdsGT_neBot sInf_image' rightLim_eq
iInf_rat_gt_eq 📖	mathematical	—	iInf Real Real.instLT Real.instRatCast Real.instInfSet toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	iInf_Ioi_eq instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Real.iInf_Ioi_eq_iInf_rat_gt mono le_of_lt
id_apply 📖	mathematical	—	toFun Real Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace id	—	—
id_leftLim 📖	mathematical	—	Function.leftLim Real Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace toFun id	—	ContinuousWithinAt.leftLim_eq instOrderTopologyReal TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace continuousWithinAt_id
instIsLocallyFiniteMeasure 📖	mathematical	—	MeasureTheory.IsLocallyFiniteMeasure measure	—	exists_Icc_mem_subset_of_mem_nhds measure_Icc
isFiniteMeasure 📖	mathematical	Filter.Tendsto Real toFun Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Filter.atTop	MeasureTheory.IsFiniteMeasure measure	—	isEmpty_or_nonempty Set.eq_empty_of_isEmpty instIsEmptySubtype MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass measure_univ
isFiniteMeasure_of_forall_abs_le 📖	mathematical	Real Real.instLE abs Real.lattice Real.instAddGroup toFun	MeasureTheory.IsFiniteMeasure measure	—	isEmpty_or_nonempty MeasureTheory.isFiniteMeasureOfIsEmpty tendsto_atTop_of_monotone instOrderTopologyReal mono Filter.Eventually.exists Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Filter.tendsto_atTop tendsto_atBot_of_monotone Filter.atBot_neBot SemilatticeInf.instIsCodirectedOrder Filter.tendsto_atBot isFiniteMeasure
isProbabilityMeasure 📖	mathematical	Filter.Tendsto Real toFun Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Filter.atTop Real.instOne	MeasureTheory.IsProbabilityMeasure measure	—	measure_univ sub_zero ENNReal.ofReal_one
length_Ioc 📖	mathematical	—	length Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ENNReal.ofReal Real Real.instSub toFun	—	length_eq le_antisymm iInf_le_of_le iInf₂_le Set.diff_subset le_iInf ENNReal.coe_le_coe le_or_gt Real.toNNReal_of_nonpos sub_nonpos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mono zero_le Set.Ioc_subset_Ioc_iff Ioc_diff_botSet Real.toNNReal_le_toNNReal sub_le_sub
length_diff_botSet 📖	mathematical	—	length Set Set.instSDiff botSet	—	isEmpty_or_nonempty length_eq_of_isEmpty length_eq iInf_congr_Prop sdiff_idem
length_empty 📖	mathematical	—	length Set Set.instEmptyCollection ENNReal instZeroENNReal	—	isEmpty_or_nonempty length_eq_of_isEmpty length_eq nonpos_iff_eq_zero ENNReal.instCanonicallyOrderedAdd iInf_le_of_le iInf_congr_Prop Set.empty_diff Set.Ioc_eq_empty Set.instReflSubset sub_self ENNReal.ofReal_zero iInf_pos instReflLe
length_eq 📖	mathematical	—	length iInf ENNReal ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Set Set.instHasSubset Set.instSDiff botSet Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ENNReal.ofReal Real Real.instSub toFun	—	iInf_congr_Prop
length_eq_of_isEmpty 📖	mathematical	—	length ENNReal instZeroENNReal	—	—
length_mono 📖	mathematical	Set Set.instHasSubset	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder length	—	isEmpty_or_nonempty length_eq_of_isEmpty instReflLe length_eq iInf_mono biInf_mono HasSubset.Subset.trans Set.instIsTransSubset Set.diff_subset_diff_left
length_subadditive_Icc_Ioo 📖	mathematical	Set Set.instHasSubset Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.iUnion Iotop	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.ofReal Real Real.instSub toFun tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	le_total ENNReal.ofReal_eq_zero sub_nonpos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mono zero_le ENNReal.instCanonicallyOrderedAdd Set.iUnion_congr_Prop le_rfl Finset.insert_erase Finset.sum_insert Finset.notMem_erase Iotop_subset_Ioc le_imp_le_of_le_of_le le_refl add_le_add_right ENNReal.instIsOrderedAddMonoid Finset.erase_ssubset Set.biUnion_insert Finset.coe_insert le_trans le_of_lt ne_of_lt le_antisymm ENNReal.ofReal_add_le ENNReal.ofReal_le_ofReal sub_add_sub_cancel sub_le_sub_right IsCompact.elim_finite_subcover_image CompactIccSpace.isCompact_Icc isOpen_Iotop Set.iUnion_true ENNReal.tsum_eq_iSup_sum le_iSup
measurableSet_Ioi 📖	mathematical	—	MeasurableSet MeasureTheory.OuterMeasure.caratheodory outer Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	MeasureTheory.OuterMeasure.ofFunction_caratheodory length_empty length_eq le_iInf length_diff_botSet Set.inter_diff_right_comm Set.diff_diff_comm le_trans add_le_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add length_mono Set.inter_subset_inter_left Set.diff_subset_diff_left le_total Set.Ioc_inter_Ioi max_eq_right Set.Ioc_eq_empty Set.Ioc_diff_Ioi min_eq_left length_Ioc zero_add min_eq_right Real.instIsOrderedAddMonoid mono sub_add_sub_cancel max_eq_left add_zero
measure_Icc 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike measure Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ENNReal.ofReal Real Real.instSub toFun Function.leftLim UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	le_or_gt Set.Icc_union_Ioc_eq_Icc le_rfl Set.Icc_self MeasureTheory.measure_union measurableSet_Ioc BorelSpace.opensMeasurable instClosedIicTopology OrderTopology.to_orderClosedTopology measure_singleton measure_Ioc covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Monotone.leftLim_le instOrderTopologyReal mono instReflLe sub_add_sub_cancel' Set.Icc_eq_empty MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass AddGroup.toOrderedSub zero_add Monotone.le_leftLim
measure_Ici 📖	mathematical	Filter.Tendsto Real toFun Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike measure Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ENNReal.ofReal Real Real.instSub Function.leftLim UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace toFun	—	Set.Icc_top measure_Icc tendsto_nhds_unique TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Filter.pure_neBot Filter.atTop_eq_pure_of_isTop isTop_top tendsto_pure_nhds NoTopOrder.to_noMaxOrder ENNReal.instT2Space Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder MeasureTheory.tendsto_measure_Ico_atTop instIsCountablyGenerated_atTop TopologicalSpace.SecondCountableTopology.to_separableSpace measure_Ico ENNReal.tendsto_ofReal Filter.Tendsto.sub_const IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal tendsto_leftLim_atTop_of_tendsto T4Space.t3Space instT4SpaceOfMetrizableSpace
measure_Ici_of_tendsto_atTop_atTop 📖	mathematical	Filter.Tendsto Real toFun Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Real.instPreorder	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike measure Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Top.top instTopENNReal	—	top_le_iff measure_Ioi_of_tendsto_atTop_atTop MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass Set.Ioi_subset_Ici_self
measure_Ico 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike measure Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ENNReal.ofReal Real Real.instSub Function.leftLim UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace toFun	—	le_or_gt Set.Ico_eq_empty MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid zero_add Monotone.leftLim instOrderTopologyReal mono Set.Icc_union_Ioo_eq_Ico le_rfl Set.Icc_self MeasureTheory.measure_union measurableSet_Ioo BorelSpace.opensMeasurable OrderTopology.to_orderClosedTopology measure_singleton measure_Ioo Monotone.leftLim_le instReflLe Monotone.le_leftLim sub_add_sub_cancel'
measure_Iic 📖	mathematical	Filter.Tendsto Real toFun Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike measure Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ENNReal.ofReal Real Real.instSub toFun	—	Set.Icc_bot measure_Icc leftLim_eq_of_isBot isBot_bot tendsto_nhds_unique TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Filter.pure_neBot Filter.atBot_eq_pure_of_isBot tendsto_pure_nhds NoBotOrder.to_noMinOrder ENNReal.instT2Space Filter.atBot_neBot SemilatticeInf.instIsCodirectedOrder MeasureTheory.tendsto_measure_Ioc_atBot instIsCountablyGenerated_atBot TopologicalSpace.SecondCountableTopology.to_separableSpace measure_Ioc ENNReal.tendsto_ofReal Filter.Tendsto.const_sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal
measure_Iic_of_tendsto_atBot_atBot 📖	mathematical	Filter.Tendsto Real toFun Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Real.instPreorder	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike measure Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Top.top instTopENNReal	—	ENNReal.eq_top_of_forall_nnreal_le Filter.eventually_atBot SemilatticeInf.instIsCodirectedOrder Filter.tendsto_atBot LE.le.trans ENNReal.ofReal_le_ofReal le_sub_comm IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid min_le_right ENNReal.coe_nnreal_eq measure_Ioc MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass Set.Ioc_subset_Iic_self
measure_Iio 📖	mathematical	Filter.Tendsto Real toFun Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike measure Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ENNReal.ofReal Real Real.instSub Function.leftLim UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace toFun	—	Set.Iic_diff_right MeasureTheory.measure_diff instReflLe MeasureTheory.nullMeasurableSet_singleton MeasureTheory.NullMeasurableSet.instMeasurableSingletonClass instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable T25Space.t2Space T3Space.t25Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space measure_singleton measure_Iic ENNReal.ofReal_sub sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Monotone.leftLim_le instOrderTopologyReal mono' le_rfl sub_sub_sub_cancel_left
measure_Iio_of_tendsto_atBot_atBot 📖	mathematical	Filter.Tendsto Real toFun Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Real.instPreorder	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike measure Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Top.top instTopENNReal	—	Filter.tendsto_pure_left Filter.atBot_eq_pure_of_isBot isBot_bot Filter.Iio_mem_atBot instNoBotOrderOfNoMinOrder instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial NoBotOrder.to_noMinOrder NoMinOrder.exists_lt top_le_iff measure_Iic_of_tendsto_atBot_atBot MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass Set.Iic_subset_Iio
measure_Ioc 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike measure Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ENNReal.ofReal Real Real.instSub toFun	—	measure_def outer_Ioc
measure_Ioi 📖	mathematical	Filter.Tendsto Real toFun Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike measure Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ENNReal.ofReal Real Real.instSub toFun	—	Set.Ici_diff_left MeasureTheory.measure_diff instReflLe MeasureTheory.nullMeasurableSet_singleton MeasureTheory.NullMeasurableSet.instMeasurableSingletonClass instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable T25Space.t2Space T3Space.t25Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space measure_singleton measure_Ici ENNReal.ofReal_sub sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Monotone.leftLim_le instOrderTopologyReal mono' le_rfl sub_sub_sub_cancel_right
measure_Ioi_of_tendsto_atTop_atTop 📖	mathematical	Filter.Tendsto Real toFun Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Real.instPreorder	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike measure Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Top.top instTopENNReal	—	ENNReal.eq_top_of_forall_nnreal_le Filter.eventually_atTop SemilatticeSup.instIsDirectedOrder Filter.tendsto_atTop LE.le.trans ENNReal.ofReal_le_ofReal le_tsub_of_add_le_right AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le le_max_right ENNReal.coe_nnreal_eq measure_Ioc MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass Set.Ioc_subset_Ioi_self
measure_Ioo 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike measure Set.Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ENNReal.ofReal Real Real.instSub Function.leftLim UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace toFun	—	le_or_gt Set.Ioo_eq_empty MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid zero_add Monotone.leftLim_le instOrderTopologyReal mono Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.zero_termg measure_Ioc ENNReal.ofReal_ne_top add_comm ENNReal.ofReal_add le_rfl Monotone.le_leftLim Set.Ioo_union_Icc_eq_Ioc Set.Icc_self MeasureTheory.measure_union MeasurableSingletonClass.measurableSet_singleton instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable T25Space.t2Space T3Space.t25Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space measure_singleton
measure_add 📖	mathematical	—	measure StieltjesFunction AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommMonoid MeasureTheory.Measure MeasureTheory.Measure.instAdd	—	MeasureTheory.Measure.ext_of_Icc instIsLocallyFiniteMeasure Filter.eq_or_neBot leftLim_eq_of_eq_bot tendsto_nhds_unique TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Monotone.tendsto_leftLim instOrderTopologyReal mono Filter.Tendsto.add IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal measure_Icc ENNReal.ofReal_add sub_nonneg_of_le covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Monotone.leftLim_le Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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.RingNF.add_assoc_rev Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg Mathlib.Tactic.RingNF.add_neg add_zero Mathlib.Tactic.Ring.add_pf_add_gt
measure_botSet 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike measure botSet instZeroENNReal	—	botSet_eq_singleton_of_isBot measure_singleton leftLim_eq_of_isBot sub_self ENNReal.ofReal_zero MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass
measure_const 📖	mathematical	—	measure const MeasureTheory.Measure MeasureTheory.Measure.instZero	—	MeasureTheory.Measure.ext_of_Icc instIsLocallyFiniteMeasure measure_Icc AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid zero_add ContinuousWithinAt.leftLim_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace continuousWithinAt_const instReflLe
measure_def 📖	mathematical	—	measure	—	—
measure_singleton 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike measure Set.instSingletonSet ENNReal.ofReal Real Real.instSub toFun Function.leftLim UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	leftLim_eq_of_eq_bot sub_self ENNReal.ofReal_zero eq_bot_iff measure_def LE.le.trans outer_le_length length_diff_botSet Set.Subsingleton.eq_singleton_of_mem subsingleton_botSet sdiff_self length_empty bot_eq_zero' ENNReal.instCanonicallyOrderedAdd instReflLe exists_seq_strictMono_tendsto' TopologicalSpace.SecondCountableTopology.to_firstCountableTopology Set.Subset.antisymm Set.mem_singleton_iff le_of_tendsto' instClosedIicTopology OrderTopology.to_orderClosedTopology Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat LT.lt.le le_antisymm MeasureTheory.tendsto_measure_iInter_atTop instIsCountablyGenerated_atTop OrderTopology.of_linearLocallyFinite instDiscreteTopologyNat TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountableNat PseudoEMetricSpace.pseudoMetrizableSpace nullMeasurableSet_Ioc BorelSpace.opensMeasurable Set.Ioc_subset_Ioc_left StrictMono.monotone measure_Ioc ENNReal.ofReal_ne_top Filter.Tendsto.comp Monotone.tendsto_leftLim instOrderTopologyReal mono tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within Filter.Eventually.of_forall ContinuousAt.tendsto Continuous.continuousAt ENNReal.continuous_ofReal Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal tendsto_const_nhds tendsto_nhds_unique ENNReal.instT2Space
measure_smul 📖	mathematical	—	measure NNReal StieltjesFunction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero instAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero NNReal.instSemiring AddCommMonoid.toAddMonoid instAddCommMonoid Module.toDistribMulAction instModuleNNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal NNReal.instCommSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right	—	MeasureTheory.Measure.ext_of_Icc IsScalarTower.right instIsLocallyFiniteMeasure measure_Icc Filter.eq_or_neBot leftLim_eq_of_eq_bot tendsto_nhds_unique TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Monotone.tendsto_leftLim instOrderTopologyReal mono Filter.Tendsto.const_smul SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal mul_sub ENNReal.ofReal_mul NNReal.zero_le_coe ENNReal.ofReal_coe_nnreal smul_eq_mul
measure_univ 📖	mathematical	Filter.Tendsto Real toFun Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Filter.atTop	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike measure Set.univ ENNReal.ofReal Real Real.instSub	—	tendsto_nhds_unique ENNReal.instT2Space Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder MeasureTheory.tendsto_measure_Iic_atTop instIsCountablyGenerated_atTop TopologicalSpace.SecondCountableTopology.to_separableSpace measure_Iic ENNReal.tendsto_ofReal Filter.Tendsto.sub_const IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal
measure_univ_of_tendsto_atBot_atBot 📖	mathematical	Filter.Tendsto Real toFun Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Real.instPreorder	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike measure Set.univ Top.top instTopENNReal	—	top_le_iff measure_Iio_of_tendsto_atBot_atBot MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass Set.subset_univ
measure_univ_of_tendsto_atTop_atTop 📖	mathematical	Filter.Tendsto Real toFun Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Real.instPreorder	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike measure Set.univ Top.top instTopENNReal	—	top_le_iff measure_Ioi_of_tendsto_atTop_atTop MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass Set.subset_univ
measure_zero 📖	mathematical	—	measure StieltjesFunction AddZero.toZero AddZeroClass.toAddZero instAddZeroClass MeasureTheory.Measure MeasureTheory.Measure.instZero	—	measure_const
mono 📖	mathematical	—	Monotone Real PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Real.instPreorder toFun	—	mono'
mono' 📖	mathematical	—	Monotone Real PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Real.instPreorder toFun	—	—
outer_Ioc 📖	mathematical	—	DFunLike.coe MeasureTheory.OuterMeasure Set ENNReal MeasureTheory.OuterMeasure.instFunLikeSetENNReal outer Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ENNReal.ofReal Real Real.instSub toFun	—	le_antisymm length_Ioc outer_le_length le_or_gt AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid zero_add mono ENNReal.instCanonicallyOrderedAdd le_iInf₂ ENNReal.le_of_forall_pos_le_add Nat.instAtLeastTwoHAddOfNat ENNReal.coe_div IsStrictOrderedRing.toCharZero LT.lt.ne' ENNReal.exists_pos_sum_of_countable instCountableNat ContinuousWithinAt.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal ContinuousWithinAt.mono right_continuous Set.Ioi_subset_Ici_self continuousWithinAt_const sub_self NNReal.coe_pos ENNReal.coe_pos nhdsGT_neBot_of_exists_gt Filter.Eventually.exists Filter.Eventually.and tendsto_order instOrderTopologyReal self_mem_nhdsWithin ENNReal.lt_add_right LT.lt.ne LE.le.trans_lt ENNReal.le_tsum ENNReal.coe_ne_zero length_eq notMem_botSet_of_lt LT.lt.trans_le ContinuousAt.comp_continuousWithinAt Continuous.continuousAt ENNReal.continuous_ofReal ENNReal.instOrderTopology HasSubset.Subset.trans Set.instIsTransSubset Set.Ioc_subset_Ioo_right Ioo_subset_Iotop Set.inter_subset_inter subset_refl Set.instReflSubset Set.inter_iUnion Set.iUnion_mono sub_add_sub_cancel ENNReal.ofReal_add_le add_le_add ENNReal.instIsOrderedAddMonoid length_subadditive_Icc_Ioo ENNReal.ofReal_le_ofReal LT.lt.le ENNReal.tsum_le_tsum ENNReal.ofReal_coe_nnreal ENNReal.tsum_add le_rfl add_assoc ENNReal.add_halves
outer_le_length 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.OuterMeasure Set MeasureTheory.OuterMeasure.instFunLikeSetENNReal outer length	—	MeasureTheory.OuterMeasure.ofFunction_le length_empty
outer_trim 📖	mathematical	—	MeasureTheory.OuterMeasure.trim outer	—	le_antisymm MeasureTheory.OuterMeasure.trim_eq_iInf le_iInf ENNReal.le_of_forall_pos_le_add ENNReal.exists_pos_sum_of_countable LT.lt.ne' ENNReal.coe_pos instCountableNat le_imp_le_of_le_of_le le_refl add_le_add_right IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid le_of_lt ENNReal.tsum_add iInf_le_of_le HasSubset.Subset.trans Set.instIsTransSubset Set.iUnion_mono ENNReal.ofReal_coe_nnreal MeasurableSet.iUnion le_trans MeasureTheory.measure_iUnion_le MeasureTheory.OuterMeasure.instOuterMeasureClass ENNReal.tsum_le_tsum isEmpty_or_nonempty Set.eq_empty_of_isEmpty instIsEmptySubtype MeasurableSet.empty MeasureTheory.measure_empty ENNReal.instCanonicallyOrderedAdd ENNReal.lt_add_right LT.lt.ne LE.le.trans_lt ENNReal.le_tsum length_eq Set.diff_subset_iff MeasurableSet.union measurableSet_botSet OpensMeasurableSpace.toMeasurableSingletonClass BorelSpace.opensMeasurable T5Space.toT1Space OrderTopology.t5Space measurableSet_Ioc instClosedIicTopology OrderTopology.to_orderClosedTopology MeasureTheory.measure_union_le add_le_add_left covariant_swap_add_of_covariant_add outer_le_length sdiff_self Set.empty_diff outer_Ioc zero_add length_empty MeasureTheory.OuterMeasure.le_trim
rightLim_eq 📖	mathematical	—	Function.rightLim Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace toFun	—	Monotone.continuousWithinAt_Ioi_iff_rightLim_eq instOrderTopologyReal mono continuousWithinAt_Ioi_iff_Ici right_continuous'
right_continuous 📖	mathematical	—	ContinuousWithinAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace toFun Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	right_continuous'
right_continuous' 📖	mathematical	—	ContinuousWithinAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace toFun Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—
zero_apply 📖	mathematical	—	toFun StieltjesFunction AddZero.toZero AddZeroClass.toAddZero instAddZeroClass Real Real.instZero	—	—

(root)

Definitions

Name	Category	Theorems
Iotop 📖	CompOp	3 math math: isOpen_Iotop, Iotop_subset_Ioc, Ioo_subset_Iotop
StieltjesFunction 📖	CompData	5 math math: StieltjesFunction.measure_zero, StieltjesFunction.zero_apply, StieltjesFunction.add_apply, StieltjesFunction.measure_add, StieltjesFunction.measure_smul
botSet 📖	CompOp	8 math math: StieltjesFunction.measure_botSet, Ioc_diff_botSet, StieltjesFunction.length_diff_botSet, StieltjesFunction.length_eq, subsingleton_botSet, measurableSet_botSet, botSet_eq_singleton_of_isBot, notMem_botSet_of_lt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Ioc_diff_botSet 📖	mathematical	—	Set Set.instSDiff Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder botSet	—	sdiff_eq_left Set.disjoint_iff_forall_ne LE.le.not_gt
Ioo_subset_Iotop 📖	mathematical	—	Set Set.instHasSubset Set.Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Iotop	—	Set.instReflSubset
Iotop_subset_Ioc 📖	mathematical	—	Set Set.instHasSubset Iotop Set.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Set.instReflSubset
botSet_eq_singleton_of_isBot 📖	mathematical	IsBot Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	botSet Set Set.instSingletonSet	—	Set.Subsingleton.eq_singleton_of_mem subsingleton_botSet
isOpen_Iotop 📖	mathematical	—	IsOpen Iotop	—	Set.Subset.antisymm instClosedIicTopology OrderTopology.to_orderClosedTopology
measurableSet_botSet 📖	mathematical	—	MeasurableSet botSet	—	Set.Subsingleton.measurableSet subsingleton_botSet
notMem_botSet_of_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Set.instMembership botSet	—	Mathlib.Tactic.Contrapose.contrapose₃
subsingleton_botSet 📖	mathematical	—	Set.Subsingleton botSet	—	Set.subsingleton_isBot

---

← Back to Index