Portmanteau

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

Statistics

Metric	Count
Definitions	0
Theorems `tendsto_measureReal_biUnion`, `tendsto_probabilityMeasure_biUnion`, `tendsto_probabilityMeasure_of_tendsto_of_mem`, `limsup_measure_closed_le_of_tendsto`, `exists_lt_measure_biUnion_of_isOpen`, `le_liminf_measure_open_of_tendsto`, `limsup_measure_closed_le_of_tendsto`, `tendsto_measure_of_isClopen_of_tendsto`, `tendsto_measure_of_null_frontier_of_tendsto`, `tendsto_measure_of_null_frontier_of_tendsto'`, `exists_null_frontier_thickening`, `exists_null_frontiers_thickening`, `integral_le_liminf_integral_of_forall_isOpen_measure_le_liminf_measure`, `le_liminf_measure_open_of_forall_tendsto_measure`, `le_measure_compl_liminf_of_limsup_measure_le`, `le_measure_liminf_of_limsup_measure_compl_le`, `limsup_measure_closed_le_iff_liminf_measure_open_ge`, `limsup_measure_closed_le_of_forall_tendsto_measure`, `limsup_measure_compl_le_of_le_liminf_measure`, `limsup_measure_le_of_le_liminf_measure_compl`, `lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure`, `tendsto_iff_forall_lipschitz_integral_tendsto`, `tendsto_measure_of_le_liminf_measure_of_limsup_measure_le`, `tendsto_measure_of_null_frontier`, `tendsto_of_forall_isClosed_limsup_le`, `tendsto_of_forall_isClosed_limsup_le'`, `tendsto_of_forall_isClosed_limsup_le_nat`, `tendsto_of_forall_isClosed_limsup_real_le'`, `tendsto_of_forall_isOpen_le_liminf`, `tendsto_of_forall_isOpen_le_liminf'`, `tendsto_of_forall_isOpen_le_liminf_nat`, `tendsto_of_forall_isOpen_le_liminf_nat'`	32
Total	32

IsPiSystem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_measureReal_biUnion` 📖	mathematical	`IsPiSystem` `Set` `Set.instMembership` `MeasurableSet` `Filter.Tendsto` `Real` `MeasureTheory.Measure.real` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`Set.iUnion` `Finset` `Finset.instMembership`	—	`MeasureTheory.measureReal_biUnion_eq_sum_powerset` `tendsto_finset_sum` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Filter.Tendsto.const_mul` `IsTopologicalSemiring.toContinuousMul` `Set.eq_empty_or_nonempty` `MeasureTheory.measureReal_empty` `tendsto_const_nhds` `biInter_mem`
`tendsto_probabilityMeasure_biUnion` 📖	mathematical	`IsPiSystem` `Set` `Set.instMembership` `MeasurableSet` `Filter.Tendsto` `NNReal` `DFunLike.coe` `MeasureTheory.ProbabilityMeasure` `MeasureTheory.ProbabilityMeasure.instFunLike` `nhds` `NNReal.instTopologicalSpace`	`Set.iUnion` `Finset` `Finset.instMembership`	—	`tendsto_measureReal_biUnion` `MeasureTheory.measure_ne_top` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `MeasureTheory.ProbabilityMeasure.instIsProbabilityMeasureToMeasure` `MeasureTheory.ProbabilityMeasure.measureReal_eq_coe_coeFn`
`tendsto_probabilityMeasure_of_tendsto_of_mem` 📖	mathematical	`IsPiSystem` `MeasurableSet` `Set` `Set.instMembership` `Filter` `Filter.instMembership` `nhds` `Set.instHasSubset` `Filter.Tendsto` `NNReal` `DFunLike.coe` `MeasureTheory.ProbabilityMeasure` `MeasureTheory.ProbabilityMeasure.instFunLike` `NNReal.instTopologicalSpace`	`MeasureTheory.ProbabilityMeasure.instTopologicalSpace`	—	`Filter.eq_or_neBot` `MeasureTheory.tendsto_of_forall_isOpen_le_liminf` `Filter.le_liminf_iff` `Filter.isCoboundedUnder_ge_of_le` `Filter.isBounded_ge_of_bot` `MeasureTheory.ProbabilityMeasure.exists_lt_measure_biUnion_of_isOpen` `tendsto_probabilityMeasure_biUnion` `Filter.mp_mem` `tendsto_order` `NNReal.instOrderTopology` `Filter.univ_mem'` `LT.lt.trans_le` `MeasureTheory.ProbabilityMeasure.apply_mono`

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_null_frontier_thickening` 📖	mathematical	`Real` `Real.instLT`	`Set` `Set.instMembership` `Set.Ioo` `Real.instPreorder` `DFunLike.coe` `Measure` `ENNReal` `Measure.instFunLike` `frontier` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Metric.thickening` `PseudoMetricSpace.toPseudoEMetricSpace` `instZeroENNReal`	—	`IsClosed.measurableSet` `isClosed_frontier` `Metric.frontier_thickening_disjoint` `Measure.countable_meas_pos_of_disjoint_iUnion` `measure_diff_null` `Measure.instOuterMeasureClass` `Set.Countable.measure_zero` `Real.noAtoms_volume` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `ENNReal.instCanonicallyOrderedAdd` `nonempty_of_measure_ne_zero` `LT.lt.ne'` `Real.volume_Ioo`
`exists_null_frontiers_thickening` 📖	mathematical	—	`Filter.Tendsto` `Real` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `Real.instLT` `DFunLike.coe` `Measure` `Set` `ENNReal` `Measure.instFunLike` `frontier` `Metric.thickening` `PseudoMetricSpace.toPseudoEMetricSpace` `instZeroENNReal`	—	`exists_seq_strictAnti_tendsto` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `exists_null_frontier_thickening` `tendsto_of_tendsto_of_tendsto_of_le_of_le` `tendsto_const_nhds` `LT.lt.le`
`integral_le_liminf_integral_of_forall_isOpen_measure_le_liminf_measure` 📖	mathematical	`IsProbabilityMeasure` `BoundedContinuousFunction` `Real` `Real.pseudoMetricSpace` `Preorder.toLE` `PartialOrder.toPreorder` `BoundedContinuousFunction.instPartialOrder` `Real.normedAddCommGroup` `Real.lattice` `BoundedContinuousFunction.instZero` `Real.instZero` `ENNReal` `ENNReal.instPartialOrder` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Filter.atTop` `Nat.instPreorder`	`Real.instLE` `integral` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `BoundedContinuousFunction.instFunLike` `Real.instConditionallyCompleteLinearOrder`	—	`lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure` `BoundedContinuousFunction.continuous` `integral_eq_lintegral_of_nonneg_ae` `Filter.Eventually.of_forall` `Measure.instOuterMeasureClass` `Measurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `instSecondCountableTopologyReal` `BorelSpace.opensMeasurable` `Real.borelSpace` `Continuous.measurable` `Real.lipschitzWith_toNNReal` `coe_nnreal_ennreal_nndist` `IsProbabilityMeasure.measure_univ` `mul_one` `BoundedContinuousFunction.lintegral_le_edist_mul` `ENNReal.liminf_toReal_eq` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `ENNReal.coe_ne_top` `ENNReal.toReal_mono` `ne_of_lt` `BoundedContinuousFunction.lintegral_nnnorm_le` `lt_of_le_of_lt` `Filter.liminf_le_of_le` `ENNReal.instCanonicallyOrderedAdd` `Filter.Eventually.exists` `le_trans` `ENNReal.ofReal_eq_coe_nnreal` `Real.norm_of_nonneg` `ENNReal.coe_lt_top`
`le_liminf_measure_open_of_forall_tendsto_measure` 📖	mathematical	`IsProbabilityMeasure` `Filter.Tendsto` `ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `nhds` `ENNReal.instTopologicalSpace` `IsOpen`	`Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	—	`le_measure_liminf_of_limsup_measure_compl_le` `IsOpen.measurableSet` `limsup_measure_closed_le_of_forall_tendsto_measure` `IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `isClosed_compl_iff`
`le_measure_compl_liminf_of_limsup_measure_le` 📖	mathematical	`IsProbabilityMeasure` `MeasurableSet` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike`	`Compl.compl` `Set.instCompl` `Filter.liminf`	—	`Filter.eq_or_neBot` `Filter.liminf_bot` `IsProbabilityMeasure.measure_univ` `measure_compl` `LT.lt.ne` `measure_lt_top` `IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `Antitone.map_limsup_of_continuousAt` `ENNReal.instOrderTopology` `antitone_const_tsub` `ENNReal.instOrderedSub` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `Continuous.continuousAt` `ENNReal.continuous_sub_left` `ENNReal.one_ne_top` `Filter.isBounded_le_of_top` `Filter.isCobounded_le_of_bot`
`le_measure_liminf_of_limsup_measure_compl_le` 📖	mathematical	`IsProbabilityMeasure` `MeasurableSet` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Compl.compl` `Set.instCompl`	`Filter.liminf`	—	`le_measure_compl_liminf_of_limsup_measure_le` `MeasurableSet.compl` `compl_compl`
`limsup_measure_closed_le_iff_liminf_measure_open_ge` 📖	mathematical	`IsProbabilityMeasure`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Filter.liminf`	—	`le_measure_liminf_of_limsup_measure_compl_le` `IsOpen.measurableSet` `isClosed_compl_iff` `limsup_measure_le_of_le_liminf_measure_compl` `IsClosed.measurableSet` `isOpen_compl_iff`
`limsup_measure_closed_le_of_forall_tendsto_measure` 📖	mathematical	`Filter.Tendsto` `ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `nhds` `ENNReal.instTopologicalSpace`	`Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	—	`Filter.eq_or_neBot` `Filter.limsup_bot` `bot_eq_zero'` `ENNReal.instCanonicallyOrderedAdd` `exists_null_frontiers_thickening` `instSFiniteOfSigmaFinite` `IsFiniteMeasure.toSigmaFinite` `Metric.isOpen_thickening` `IsOpen.measurableSet` `ENNReal.le_of_forall_pos_le_add` `tendsto_measure_cthickening_of_isClosed` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `measure_ne_top` `Iio_mem_nhds` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `ENNReal.lt_add_right` `LT.lt.ne` `LT.lt.ne'` `ENNReal.coe_pos` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.Eventually.of_forall` `measure_mono` `Measure.instOuterMeasureClass` `Metric.self_subset_thickening` `LE.le.trans` `Filter.limsup_le_limsup` `Filter.isCobounded_le_of_bot` `Filter.isBounded_le_of_top` `Filter.Tendsto.limsup_eq` `Metric.thickening_subset_cthickening` `LT.lt.le` `Eq.le`
`limsup_measure_compl_le_of_le_liminf_measure` 📖	mathematical	`IsProbabilityMeasure` `MeasurableSet` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	`Filter.limsup` `Compl.compl` `Set.instCompl`	—	`Filter.eq_or_neBot` `Filter.limsup_bot` `IsProbabilityMeasure.measure_univ` `measure_compl` `LT.lt.ne` `measure_lt_top` `IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `Antitone.map_liminf_of_continuousAt` `ENNReal.instOrderTopology` `antitone_const_tsub` `ENNReal.instOrderedSub` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `Continuous.continuousAt` `ENNReal.continuous_sub_left` `ENNReal.one_ne_top` `Filter.isCobounded_ge_of_top` `Filter.isBounded_ge_of_bot`
`limsup_measure_le_of_le_liminf_measure_compl` 📖	mathematical	`IsProbabilityMeasure` `MeasurableSet` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Compl.compl` `Set.instCompl` `Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	`Filter.limsup`	—	`limsup_measure_compl_le_of_le_liminf_measure` `MeasurableSet.compl` `compl_compl`
`lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure` 📖	mathematical	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Pi.hasLe` `Real.instLE` `Pi.instZero` `Real.instZero` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Filter.atTop` `Nat.instPreorder`	`lintegral` `ENNReal.ofReal`	—	`lintegral_eq_lintegral_meas_lt` `Filter.Eventually.of_forall` `Measure.instOuterMeasureClass` `Continuous.aemeasurable` `Real.borelSpace` `LE.le.trans` `lintegral_mono` `continuous_def` `isOpen_Ioi` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `le_refl` `lintegral_liminf_le` `Antitone.measurable` `ENNReal.borelSpace` `ENNReal.instOrderTopology` `ENNReal.instSecondCountableTopology` `measure_mono` `lt_of_le_of_lt`
`tendsto_iff_forall_lipschitz_integral_tendsto` 📖	mathematical	—	`Filter.Tendsto` `ProbabilityMeasure` `nhds` `ProbabilityMeasure.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Real` `integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `ProbabilityMeasure.toMeasure` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`LipschitzWith.continuous` `Filter.eq_or_neBot` `tendsto_of_forall_isClosed_limsup_real_le'` `le_of_forall_pos_le_add` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `div_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `Nat.cast_nonneg'` `Real.instZeroLEOneClass` `tendsto_integral_thickenedIndicator_of_isClosed` `IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `ProbabilityMeasure.instIsProbabilityMeasureToMeasure` `tendsto_one_div_add_atTop_nhds_zero_nat` `RCLike.charZero_rclike` `NNRat.instContinuousSMulOfIsScalarTowerOfRat` `IsScalarTower.nnrat` `Rat.instCharZero` `NNRat.instContinuousSMulRatReal` `Nat.instAtLeastTwoHAddOfNat` `ProbabilityMeasure.measureReal_eq_coe_coeFn` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.Tendsto.eventually_lt_const` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `thickenedIndicator_le_one` `one_div` `thickenedIndicator.congr_simp` `lipschitzWith_thickenedIndicator` `Filter.Eventually.mono` `Filter.Tendsto.eventually_le_const` `le_trans` `integral_indicator_one` `IsClosed.measurableSet` `integral_mono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `integrable_indicator_iff` `Integrable.integrableOn` `integrable_const` `integrable_thickenedIndicator` `indicator_le_thickenedIndicator` `NNReal.coe_indicator` `LE.le.trans` `Filter.limsup_le_of_le` `Filter.isCoboundedUnder_le_of_le` `LE.le.trans_eq` `add_le_add` `LT.lt.le` `Eq.le` `le_refl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz`
`tendsto_measure_of_le_liminf_measure_of_limsup_measure_le` 📖	mathematical	`Set` `Set.instHasSubset` `DFunLike.coe` `Measure` `ENNReal` `Measure.instFunLike` `Set.instSDiff` `instZeroENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Filter.limsup`	`Filter.Tendsto` `nhds` `ENNReal.instTopologicalSpace`	—	`tendsto_of_le_liminf_of_limsup_le` `ENNReal.instOrderTopology` `Measure.instOuterMeasureClass` `Filter.EventuallyLE.antisymm` `HasSubset.Subset.eventuallyLE` `Filter.EventuallyLE.trans` `ae_le_set` `measure_congr` `Filter.EventuallyEq.symm` `Filter.liminf_le_liminf` `Filter.Eventually.of_forall` `measure_mono` `Filter.isBounded_ge_of_bot` `Filter.isCobounded_ge_of_top` `Filter.limsup_le_limsup` `Filter.isCobounded_le_of_bot` `Filter.isBounded_le_of_top`
`tendsto_measure_of_null_frontier` 📖	mathematical	`IsProbabilityMeasure` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `frontier` `instZeroENNReal`	`Filter.Tendsto` `nhds` `ENNReal.instTopologicalSpace`	—	`tendsto_measure_of_le_liminf_measure_of_limsup_measure_le` `interior_subset` `subset_closure` `isOpen_interior` `limsup_measure_closed_le_iff_liminf_measure_open_ge` `isClosed_closure`
`tendsto_of_forall_isClosed_limsup_le` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `NNReal.instConditionallyCompleteLinearOrderBot` `DFunLike.coe` `ProbabilityMeasure` `Set` `ProbabilityMeasure.instFunLike`	`Filter.Tendsto` `nhds` `ProbabilityMeasure.instTopologicalSpace`	—	`Filter.tendsto_of_seq_tendsto` `tendsto_of_forall_isClosed_limsup_le_nat` `le_trans` `Eq.trans_le` `Filter.limsup_comp` `Filter.limsup_le_limsup_of_le` `Filter.isCobounded_le_of_bot`
`tendsto_of_forall_isClosed_limsup_le'` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `ProbabilityMeasure.toMeasure`	`Filter.Tendsto` `ProbabilityMeasure` `nhds` `ProbabilityMeasure.instTopologicalSpace`	—	`tendsto_of_forall_isOpen_le_liminf'` `limsup_measure_closed_le_iff_liminf_measure_open_ge` `ProbabilityMeasure.instIsProbabilityMeasureToMeasure`
`tendsto_of_forall_isClosed_limsup_le_nat` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `NNReal.instConditionallyCompleteLinearOrderBot` `DFunLike.coe` `ProbabilityMeasure` `Set` `ProbabilityMeasure.instFunLike` `Filter.atTop` `Nat.instPreorder`	`Filter.Tendsto` `nhds` `ProbabilityMeasure.instTopologicalSpace`	—	`tendsto_of_forall_isClosed_limsup_le'` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat` `PseudoEMetricSpace.pseudoMetrizableSpace` `Monotone.map_limsup_of_continuousAt` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `NNReal.instOrderTopology` `ENNReal.instOrderTopology` `ENNReal.coe_mono` `Continuous.continuousAt` `ENNReal.continuous_coe` `NNReal.instCanonicallyOrderedAdd` `ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure`
`tendsto_of_forall_isClosed_limsup_real_le'` 📖	mathematical	`Real` `Real.instLE` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Real.instConditionallyCompleteLinearOrder` `Measure.real` `ProbabilityMeasure.toMeasure`	`Filter.Tendsto` `ProbabilityMeasure` `nhds` `ProbabilityMeasure.instTopologicalSpace`	—	`tendsto_of_forall_isClosed_limsup_le` `ProbabilityMeasure.measureReal_eq_coe_coeFn` `NNReal.toReal_limsup`
`tendsto_of_forall_isOpen_le_liminf` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `ProbabilityMeasure` `Set` `ProbabilityMeasure.instFunLike` `Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `NNReal.instConditionallyCompleteLinearOrderBot`	`Filter.Tendsto` `nhds` `ProbabilityMeasure.instTopologicalSpace`	—	`Filter.tendsto_of_seq_tendsto` `tendsto_of_forall_isOpen_le_liminf_nat` `LE.le.trans` `Filter.liminf_comp` `Filter.liminf_le_liminf_of_le` `Filter.isBounded_ge_of_bot` `Filter.IsBoundedUnder.isCoboundedUnder_ge` `Filter.map_neBot` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.isBoundedUnder_of`
`tendsto_of_forall_isOpen_le_liminf'` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `ProbabilityMeasure.toMeasure` `Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	`Filter.Tendsto` `ProbabilityMeasure` `nhds` `ProbabilityMeasure.instTopologicalSpace`	—	`Filter.tendsto_of_seq_tendsto` `tendsto_of_forall_isOpen_le_liminf_nat'` `LE.le.trans` `Filter.liminf_le_liminf_of_le` `Filter.isBounded_ge_of_bot` `Filter.isCobounded_ge_of_top`
`tendsto_of_forall_isOpen_le_liminf_nat` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `ProbabilityMeasure` `Set` `ProbabilityMeasure.instFunLike` `Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `NNReal.instConditionallyCompleteLinearOrderBot` `Filter.atTop` `Nat.instPreorder`	`Filter.Tendsto` `nhds` `ProbabilityMeasure.instTopologicalSpace`	—	`tendsto_of_forall_isOpen_le_liminf_nat'` `Monotone.map_liminf_of_continuousAt` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `NNReal.instOrderTopology` `ENNReal.instOrderTopology` `ENNReal.coe_mono` `Continuous.continuousAt` `ENNReal.continuous_coe` `Filter.IsBoundedUnder.isCoboundedUnder_ge` `NNReal.instCanonicallyOrderedAdd` `ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure`
`tendsto_of_forall_isOpen_le_liminf_nat'` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `ProbabilityMeasure.toMeasure` `Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Filter.atTop` `Nat.instPreorder`	`Filter.Tendsto` `ProbabilityMeasure` `nhds` `ProbabilityMeasure.instTopologicalSpace`	—	`ProbabilityMeasure.tendsto_iff_forall_integral_tendsto` `BoundedContinuousFunction.tendsto_integral_of_forall_integral_le_liminf_integral` `ProbabilityMeasure.instIsProbabilityMeasureToMeasure` `integral_le_liminf_integral_of_forall_isOpen_measure_le_liminf_measure`

MeasureTheory.FiniteMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`limsup_measure_closed_le_of_tendsto` 📖	mathematical	`Filter.Tendsto` `MeasureTheory.FiniteMeasure` `nhds` `instTopologicalSpace`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `toMeasure`	—	`Filter.eq_or_neBot` `Filter.limsup_bot` `ENNReal.le_of_forall_pos_le_add` `Nat.instAtLeastTwoHAddOfNat` `LT.lt.ne` `ENNReal.half_pos` `ENNReal.coe_ne_zero` `HasOuterApproxClosed.tendsto_lintegral_apprSeq` `isFiniteMeasure` `ENNReal.lt_add_right` `MeasureTheory.measure_lt_top` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.Tendsto.eventually_lt_const` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `tendsto_iff_forall_lintegral_tendsto` `ne_of_lt` `BoundedContinuousFunction.lintegral_lt_top_of_nnreal` `Filter.Tendsto.eventually_le_const` `Filter.Eventually.mono` `le_trans` `HasOuterApproxClosed.measure_le_lintegral` `LE.le.trans` `Filter.limsup_le_limsup` `Filter.isCobounded_le_of_bot` `Filter.isBounded_le_of_top` `Filter.limsup_const` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `LT.lt.le` `Eq.le` `le_refl` `add_assoc` `ENNReal.add_halves`

MeasureTheory.ProbabilityMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_lt_measure_biUnion_of_isOpen` 📖	mathematical	`Set` `Set.instMembership` `Filter` `Filter.instMembership` `nhds` `Set.instHasSubset` `IsOpen` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `MeasureTheory.ProbabilityMeasure` `instFunLike`	`Set.iUnion` `Finset` `Finset.instMembership`	—	`TopologicalSpace.isOpen_iUnion_countable` `isOpen_interior` `Set.Countable.image` `Set.Subset.antisymm` `Set.iUnion_congr_Prop` `Set.iUnion_exists` `Set.iUnion_coe_set` `mem_interior_iff_mem_nhds` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.biUnion_image` `Set.iUnion₂_mono` `interior_subset` `Mathlib.Tactic.Contrapose.contrapose₁` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `coeFn_empty` `NNReal.instCanonicallyOrderedAdd` `Set.Countable.exists_eq_range` `Set.iUnion_iUnion_eq'` `ENNReal.tendsto_toNNReal_iff` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `instIsProbabilityMeasureToMeasure` `MeasureTheory.tendsto_measure_iUnion_accumulate` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat` `PseudoEMetricSpace.pseudoMetrizableSpace` `Filter.Eventually.exists` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `tendsto_order` `NNReal.instOrderTopology` `Nat.instNoMaxOrder` `Set.biUnion_and'` `Set.iUnion_iUnion_eq_right` `Set.subset_iUnion`
`le_liminf_measure_open_of_tendsto` 📖	mathematical	`Filter.Tendsto` `MeasureTheory.ProbabilityMeasure` `nhds` `instTopologicalSpace` `IsOpen`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `toMeasure` `Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	—	`MeasureTheory.le_measure_liminf_of_limsup_measure_compl_le` `instIsProbabilityMeasureToMeasure` `IsOpen.measurableSet` `limsup_measure_closed_le_of_tendsto` `isClosed_compl_iff`
`limsup_measure_closed_le_of_tendsto` 📖	mathematical	`Filter.Tendsto` `MeasureTheory.ProbabilityMeasure` `nhds` `instTopologicalSpace`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `toMeasure`	—	`MeasureTheory.FiniteMeasure.limsup_measure_closed_le_of_tendsto` `tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds`
`tendsto_measure_of_isClopen_of_tendsto` 📖	mathematical	`Filter.Tendsto` `MeasureTheory.ProbabilityMeasure` `nhds` `instTopologicalSpace` `IsClopen`	`NNReal` `DFunLike.coe` `Set` `instFunLike` `NNReal.instTopologicalSpace`	—	`tendsto_measure_of_null_frontier_of_tendsto` `IsClopen.frontier_eq` `coeFn_empty`
`tendsto_measure_of_null_frontier_of_tendsto` 📖	mathematical	`Filter.Tendsto` `MeasureTheory.ProbabilityMeasure` `nhds` `instTopologicalSpace` `DFunLike.coe` `Set` `NNReal` `instFunLike` `frontier` `instZeroNNReal`	`NNReal.instTopologicalSpace`	—	`tendsto_measure_of_null_frontier_of_tendsto'` `Filter.Tendsto.comp` `ENNReal.tendsto_toNNReal` `MeasureTheory.measure_ne_top` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `instIsProbabilityMeasureToMeasure`
`tendsto_measure_of_null_frontier_of_tendsto'` 📖	mathematical	`Filter.Tendsto` `MeasureTheory.ProbabilityMeasure` `nhds` `instTopologicalSpace` `DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure` `frontier` `instZeroENNReal`	`ENNReal.instTopologicalSpace`	—	`MeasureTheory.tendsto_measure_of_null_frontier` `instIsProbabilityMeasureToMeasure` `le_liminf_measure_open_of_tendsto`

---

← Back to Index