Documentation Verification Report

LevyConvergence

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

Statistics

Metric	Count
Definitions	0
Theorems `tendsto_charPoly_of_tendsto_charFun`, `tendsto_iff_tendsto_charFun`, `tendsto_of_tendsto_charFun`, `tendsto_of_tight_of_separatesPoints`, `isTightMeasureSet_of_tendsto_charFun`	5
Total	5

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isTightMeasureSet_of_tendsto_charFun` 📖	mathematical	`IsProbabilityMeasure` `ContinuousAt` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Filter.Tendsto` `charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `Filter.atTop` `Nat.instPreorder` `nhds`	`IsTightMeasureSet` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.range` `Measure`	—	`isTightMeasureSet_range_of_tendsto_limsup_measureReal_inner_of_norm_eq_one` `IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `Nat.instAtLeastTwoHAddOfNat` `neg_le_self_iff` `Real.instIsOrderedAddMonoid` `le_of_lt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `neg_mul` `le_imp_le_of_le_of_le` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `intervalIntegral.norm_integral_le_integral_norm` `le_refl` `intervalIntegral.integral_of_le` `integral_mono_of_nonneg` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `ae_of_all` `Measure.instOuterMeasureClass` `norm_nonneg` `integrable_const` `Real.isFiniteMeasure_restrict_Ioc` `norm_one_sub_charFun_le_two` `intervalIntegral.integral_const` `Real.instCompleteSpace` `sub_neg_eq_add` `Mathlib.Tactic.FieldSimp.le_eq_cancel_le` `PosMulStrictMono.toPosMulMono` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Meta.NormNum.isNat_le_true` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.isNat_add` `Nat.cast_one` `measureReal_abs_inner_gt_le_integral_charFun` `BorelSpace.opensMeasurable` `Filter.limsup_le_limsup` `Filter.Eventually.of_forall` `Filter.IsCoboundedUnder.of_frequently_ge` `Filter.Frequently.of_forall` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `ENNReal.toReal_nonneg` `Filter.Tendsto.limsup_eq` `instOrderTopologyReal` `Filter.Tendsto.const_mul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Filter.Tendsto.norm` `tendsto_integral_of_dominated_convergence` `Measurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `UniformSpace.secondCountable_of_separable` `EMetric.instIsCountablyGeneratedUniformity` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `Complex.instProperSpace` `Complex.borelSpace` `Measurable.const_sub` `ContinuousSub.measurableSub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Measurable.fun_comp` `measurable_charFun` `FiniteDimensional.proper_real` `instSFiniteOfSigmaFinite` `sigmaFinite_of_locallyFinite` `IsFiniteMeasure.toIsLocallyFiniteMeasure` `Measurable.smul_const` `ContinuousSMul.toMeasurableSMul` `Real.borelSpace` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `measurable_id'` `Filter.Tendsto.sub` `tendsto_const_nhds` `tendsto_of_tendsto_of_tendsto_of_le_of_le'` `ContinuousAt.tendsto` `Metric.tendsto_atTop` `charFun_zero` `probReal_univ` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `dist_zero_right` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_inv` `Real.norm_ofNat` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `dist_eq_norm_sub'` `zero_sub` `norm_neg` `Metric.tendsto_nhds_nhds` `div_pos` `lt_of_lt_of_le` `LT.lt.le` `norm_smul` `NormedSpace.toNormSMulClass` `lt_div_iff₀'` `inv_lt_comm₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Mathlib.Tactic.FieldSimp.lt_eq_cancel_lt` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.cons_pos` `Mathlib.Meta.NormNum.isNat_lt_true` `RCLike.charZero_rclike` `measurable_of_tendsto_metrizable` `tendsto_pi_nhds` `integral_mono_ae` `Integrable.mono'` `instSecondCountableTopologyReal` `Measurable.norm` `norm_norm` `ae_restrict_eq` `instClosedIicTopology` `ae_restrict_of_forall_mem` `measurableSet_Ioc` `intervalIntegral.integral_div` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Meta.NormNum.isNat_eq_false` `Nat.cast_zero` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Filter.mp_mem` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Filter.univ_mem'` `Filter.le_limsup_of_le` `LE.le.trans` `Filter.Eventually.exists` `IsProbabilityMeasure.measure_univ` `instReflLe`

MeasureTheory.ProbabilityMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_charPoly_of_tendsto_charFun` 📖	mathematical	`Filter.Tendsto` `Complex` `MeasureTheory.charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `toMeasure` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `StarSubalgebra` `Complex.instCommSemiring` `Complex.instStarRing` `BoundedContinuousFunction.instSemiring` `Complex.instSemiring` `instBoundedMul` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instBoundedAddOfLipschitzAdd` `ESeminormedAddMonoid.toAddMonoid` `Complex.instNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `BoundedContinuousFunction.instStarRing` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `CStarRing.to_normedStarGroup` `RCLike.instCStarRing` `Complex.instRCLike` `BoundedContinuousFunction.instAlgebra` `NormedCommRing.toNormedRing` `NormedAlgebra.id` `BoundedContinuousFunction.instStarModule` `StarRing.toStarAddMonoid` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `StarMul.toStarModule` `CommRing.toCommMonoid` `Complex.commRing` `StarRing.toStarMul` `SetLike.instMembership` `StarSubalgebra.setLike` `BoundedContinuousFunction.charPoly` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `Real.probChar` `innerₗ` `Real.continuous_probChar` `continuous_inner`	`Filter.Tendsto` `Complex` `MeasureTheory.integral` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `toMeasure` `DFunLike.coe` `BoundedContinuousFunction` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `BoundedContinuousFunction.instFunLike` `nhds`	—	`instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `CStarRing.to_normedStarGroup` `RCLike.instCStarRing` `BoundedContinuousFunction.instStarModule` `StarMul.toStarModule` `Real.continuous_probChar` `continuous_inner` `Algebra.to_smulCommClass` `BoundedContinuousFunction.mem_charPoly` `MeasureTheory.integral_finset_sum` `MeasureTheory.Integrable.const_mul` `BoundedContinuousFunction.integrable` `BorelSpace.opensMeasurable` `UniformSpace.secondCountable_of_separable` `EMetric.instIsCountablyGeneratedUniformity` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `Complex.instProperSpace` `Complex.borelSpace` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `MeasureTheory.integral_const_mul` `instIsProbabilityMeasureToMeasure` `tendsto_finset_sum` `Filter.Tendsto.const_mul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul`
`tendsto_iff_tendsto_charFun` 📖	mathematical	—	`Filter.Tendsto` `MeasureTheory.ProbabilityMeasure` `Filter.atTop` `Nat.instPreorder` `nhds` `instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `BorelSpace.opensMeasurable` `Complex` `MeasureTheory.charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `toMeasure` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	—	`BorelSpace.opensMeasurable` `MeasureTheory.charFun_eq_integral_innerProbChar` `tendsto_iff_forall_integral_rclike_tendsto` `tendsto_of_tendsto_charFun`
`tendsto_of_tendsto_charFun` 📖	mathematical	`Filter.Tendsto` `Complex` `MeasureTheory.charFun` `InnerProductSpace.toInner` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `toMeasure` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	`Filter.Tendsto` `MeasureTheory.ProbabilityMeasure` `Filter.atTop` `Nat.instPreorder` `nhds` `instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `BorelSpace.opensMeasurable`	—	`MeasureTheory.isTightMeasureSet_of_tendsto_charFun` `instIsProbabilityMeasureToMeasure` `Continuous.continuousAt` `MeasureTheory.continuous_charFun` `secondCountable_of_proper` `FiniteDimensional.proper_real` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `tendsto_of_tight_of_separatesPoints` `instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable` `complete_of_proper` `EMetric.instIsCountablyGeneratedUniformity` `T6Space.toT0Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `Real.continuous_probChar` `continuous_inner` `BoundedContinuousFunction.separatesPoints_charPoly` `Real.probChar_ne_one` `Algebra.to_smulCommClass` `DFunLike.ne_iff` `inner_self_ne_zero` `tendsto_charPoly_of_tendsto_charFun`
`tendsto_of_tight_of_separatesPoints` 📖	mathematical	`MeasureTheory.IsTightMeasureSet` `setOf` `MeasureTheory.Measure` `toMeasure` `Subalgebra.SeparatesPoints` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Ring.toSemiring` `NormedRing.toRing` `NormedAlgebra.toAlgebra` `NormedAlgebra.id` `IsTopologicalRing.toIsTopologicalSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `StarSubalgebra.toSubalgebra` `ContinuousMap` `RCLike.toStarRing` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `ContinuousMap.instStarRingOfContinuousStar` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `RCLike.instContinuousStar` `ContinuousMap.algebra` `ContinuousMap.instStarModule` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `StarRing.toStarAddMonoid` `Algebra.toSMul` `StarMul.toStarModule` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `CommRing.toRing` `StarSubalgebra.map` `BoundedContinuousFunction` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `BoundedContinuousFunction.instSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instBoundedMul` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `IsTopologicalSemiring.toContinuousMul` `instBoundedAddOfLipschitzAdd` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SeminormedAddCommGroup.to_lipschitzAdd` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `BoundedContinuousFunction.instStarRing` `CStarRing.to_normedStarGroup` `RCLike.instCStarRing` `BoundedContinuousFunction.instAlgebra` `BoundedContinuousFunction.instStarModule` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `BoundedContinuousFunction.toContinuousMapStarₐ` `Filter.Tendsto` `MeasureTheory.integral` `Real` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `DFunLike.coe` `BoundedContinuousFunction.instFunLike` `nhds`	`Filter.Tendsto` `MeasureTheory.ProbabilityMeasure` `nhds` `instTopologicalSpace` `BorelSpace.opensMeasurable`	—	`instBoundedMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `instBoundedAddOfLipschitzAdd` `SeminormedAddCommGroup.to_lipschitzAdd` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `CStarRing.to_normedStarGroup` `RCLike.instCStarRing` `BoundedContinuousFunction.instStarModule` `StarMul.toStarModule` `NonUnitalSeminormedRing.toIsTopologicalRing` `RCLike.instContinuousStar` `ContinuousMap.instStarModule` `BorelSpace.opensMeasurable` `Filter.eq_or_neBot` `Filter.tendsto_iff_ultrafilter` `isCompact_closure_of_isTightMeasureSet` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `PolishSpace.toIsCompletelyMetrizableSpace` `IsCompact.ultrafilter_le_nhds` `LE.le.trans` `Filter.monotone_principal` `subset_closure` `MeasureTheory.ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable` `TopologicalSpace.UpgradedIsCompletelyMetrizableSpace.toCompleteSpace` `PolishSpace.toSecondCountableTopology` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `instIsProbabilityMeasureToMeasure` `tendsto_nhds_unique` `Ultrafilter.neBot` `tendsto_iff_forall_integral_rclike_tendsto` `Filter.Tendsto.comp` `eq_of_forall_toMeasure_apply_eq`

---

← Back to Index