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 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	96 math math: ProbabilityTheory.stieltjesOfMeasurableRat_ae_eq, ProbabilityTheory.paretoCDFReal_eq_lintegral, 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.gammaCDFReal_eq_lintegral, 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.gammaCDFReal_eq_integral, 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, zero_apply, add_apply, ProbabilityTheory.stronglyMeasurable_stieltjesOfMeasurableRat, mono, ProbabilityTheory.IsCondKernelCDF.measurable, ProbabilityTheory.tendsto_stieltjesOfMeasurableRat_atBot, ProbabilityTheory.measurable_stieltjesOfMeasurableRat, ProbabilityTheory.exponentialCDFReal_eq_integral, ProbabilityTheory.stieltjesOfMeasurableRat_eq, ProbabilityTheory.cdf_expMeasure_eq_integral, ProbabilityTheory.paretoCDFReal_eq_integral, ProbabilityTheory.IsCondKernelCDF.integrable, ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunction_eq, ProbabilityTheory.IsMeasurableRatCDF.measure_stieltjesFunction_Iic, ProbabilityTheory.IsCondKernelCDF.tendsto_atBot_zero, ext_iff, ProbabilityTheory.exponentialCDFReal_eq, 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, 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, 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.exponentialCDFReal_eq_lintegral, 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 NNReal.instCanonicallyOrderedAdd 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
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	—	—
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 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 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 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 ENNReal.ofReal Real.instSub Function.leftLim	—	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_order instOrderTopologyReal NoMaxOrder.exists_gt LT.lt.trans_le le_rfl Monotone.le_leftLim mono Filter.mp_mem Filter.univ_mem' LE.le.trans_lt Monotone.leftLim_le
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 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 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 ENNReal.ofReal Real.instSub	—	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 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 ENNReal.ofReal Real.instSub Function.leftLim	—	Set.Iic_diff_right MeasureTheory.measure_diff 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 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 ENNReal.ofReal Real.instSub	—	Set.Ici_diff_left MeasureTheory.measure_diff 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 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 AddLeftCancelSemigroup.toIsLeftCancelAdd 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 IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring 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.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg add_zero Mathlib.Tactic.RingNF.add_neg Mathlib.Tactic.RingNF.add_assoc_rev 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
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 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 instSemiringNNReal AddCommMonoid.toAddMonoid instAddCommMonoid Module.toDistribMulAction instModuleNNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal instCommSemiringNNReal 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 IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring 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.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 NNReal.instIsStrictOrderedRing 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