Documentation Verification Report

TightNormed

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

Statistics

Metric	Count
Definitions	0
Theorems `isTightMeasureSet_iff_inner_tendsto`, `isTightMeasureSet_iff_tendsto_measure_compl_closedBall`, `isTightMeasureSet_iff_tendsto_measure_norm_gt`, `isTightMeasureSet_of_forall_basis_tendsto`, `isTightMeasureSet_of_inner_tendsto`, `isTightMeasureSet_of_tendsto_measure_compl_closedBall`, `isTightMeasureSet_of_tendsto_measure_norm_gt`, `isTightMeasureSet_range_iff_tendsto_limsup_inner`, `isTightMeasureSet_range_iff_tendsto_limsup_measure_norm_gt`, `isTightMeasureSet_range_of_tendsto_limsup_inner`, `isTightMeasureSet_range_of_tendsto_limsup_inner_of_norm_eq_one`, `isTightMeasureSet_range_of_tendsto_limsup_measureReal_inner_of_norm_eq_one`, `isTightMeasureSet_range_of_tendsto_limsup_measure_norm_gt`, `tendsto_measure_compl_closedBall_of_isTightMeasureSet`, `tendsto_measure_norm_gt_of_isTightMeasureSet`	15
Total	15

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isTightMeasureSet_iff_inner_tendsto` 📖	mathematical	—	`IsTightMeasureSet` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.Tendsto` `Real` `ENNReal` `iSup` `Measure` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set` `Set.instMembership` `DFunLike.coe` `Measure.instFunLike` `setOf` `Real.instLT` `Norm.norm` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Inner.inner` `InnerProductSpace.toInner` `Filter.atTop` `Real.instPreorder` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`FiniteDimensional.proper` `locallyCompact_of_proper` `FiniteDimensional.proper_real` `FiniteDimensional.rclike_to_real` `iSup_congr_Prop` `inner_zero_left` `Filter.tendsto_congr'` `Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `norm_zero` `not_lt` `measure_empty` `Measure.instOuterMeasureClass` `ENNReal.iSup_zero` `ciSup_const` `tendsto_const_nhds` `Filter.Tendsto.comp` `isTightMeasureSet_iff_tendsto_measure_norm_gt` `Filter.tendsto_mul_const_atTop_of_pos` `Real.instIsStrictOrderedRing` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `norm_pos_iff` `Filter.tendsto_id` `tendsto_of_tendsto_of_tendsto_of_le_of_le` `ENNReal.instOrderTopology` `zero_le` `ENNReal.instCanonicallyOrderedAdd` `measure_mono` `mul_inv_lt_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `mul_comm` `LT.lt.trans_le` `norm_inner_le_norm` `iSup₂_le_iff` `le_iSup_of_le` `iSup_pos` `isTightMeasureSet_of_inner_tendsto`
`isTightMeasureSet_iff_tendsto_measure_compl_closedBall` 📖	mathematical	—	`IsTightMeasureSet` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Filter.Tendsto` `Real` `ENNReal` `iSup` `Measure` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set` `Set.instMembership` `DFunLike.coe` `Measure.instFunLike` `Compl.compl` `Set.instCompl` `Metric.closedBall` `Filter.atTop` `Real.instPreorder` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`tendsto_measure_compl_closedBall_of_isTightMeasureSet` `isTightMeasureSet_of_tendsto_measure_compl_closedBall`
`isTightMeasureSet_iff_tendsto_measure_norm_gt` 📖	mathematical	—	`IsTightMeasureSet` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.Tendsto` `Real` `ENNReal` `iSup` `Measure` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set` `Set.instMembership` `DFunLike.coe` `Measure.instFunLike` `setOf` `Real.instLT` `Norm.norm` `NormedAddCommGroup.toNorm` `Filter.atTop` `Real.instPreorder` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`tendsto_measure_norm_gt_of_isTightMeasureSet` `isTightMeasureSet_of_tendsto_measure_norm_gt`
`isTightMeasureSet_of_forall_basis_tendsto` 📖	mathematical	`Filter.Tendsto` `Real` `ENNReal` `iSup` `Measure` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set` `Set.instMembership` `DFunLike.coe` `Measure.instFunLike` `setOf` `Real.instLT` `Norm.norm` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `OrthonormalBasis` `OrthonormalBasis.instFunLike` `Filter.atTop` `Real.instPreorder` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	`IsTightMeasureSet` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`subsingleton_or_nontrivial` `Filter.cocompact_eq_bot` `TopologicalSpace.NoetherianSpace.compactSpace` `TopologicalSpace.Finite.to_noetherianSpace` `Finite.of_subsingleton` `Filter.smallSets_bot` `iSup_apply` `iSup_congr_Prop` `measure_empty` `Measure.instOuterMeasureClass` `ENNReal.iSup_zero` `ciSup_const` `tendsto_pure_nhds` `Module.finrank_eq_card_basis` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Real.instIsOrderedRing` `Real.instNontrivial` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `FiniteDimensional.proper` `locallyCompact_of_proper` `FiniteDimensional.proper_real` `FiniteDimensional.rclike_to_real` `isTightMeasureSet_of_tendsto_measure_norm_gt` `iSup_mono` `measure_mono` `LT.lt.trans_le` `OrthonormalBasis.norm_le_card_mul_iSup_norm_inner` `lt_irrefl` `div_lt_iff₀'` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.sqrt_pos_of_pos` `ciSup_le` `measure_iUnion_fintype_le` `iSup_le` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `le_biSup` `tendsto_of_tendsto_of_tendsto_of_le_of_le` `ENNReal.instOrderTopology` `tendsto_const_nhds` `Finset.sum_const_zero` `tendsto_finset_sum` `ENNReal.instContinuousAdd` `Filter.Tendsto.comp` `Filter.Tendsto.atTop_div_const` `Filter.tendsto_id` `zero_le` `ENNReal.instCanonicallyOrderedAdd`
`isTightMeasureSet_of_inner_tendsto` 📖	mathematical	`Filter.Tendsto` `Real` `ENNReal` `iSup` `Measure` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set` `Set.instMembership` `DFunLike.coe` `Measure.instFunLike` `setOf` `Real.instLT` `Norm.norm` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.atTop` `Real.instPreorder` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	`IsTightMeasureSet` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`isTightMeasureSet_of_forall_basis_tendsto`
`isTightMeasureSet_of_tendsto_measure_compl_closedBall` 📖	mathematical	`Filter.Tendsto` `Real` `ENNReal` `iSup` `Measure` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set` `Set.instMembership` `DFunLike.coe` `Measure.instFunLike` `Compl.compl` `Set.instCompl` `Metric.closedBall` `Filter.atTop` `Real.instPreorder` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	`IsTightMeasureSet` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	`isTightMeasureSet_iff_exists_isCompact_measure_compl_le` `ENNReal.tendsto_atTop_zero` `ProperSpace.isCompact_closedBall` `le_rfl`
`isTightMeasureSet_of_tendsto_measure_norm_gt` 📖	mathematical	`Filter.Tendsto` `Real` `ENNReal` `iSup` `Measure` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set` `Set.instMembership` `DFunLike.coe` `Measure.instFunLike` `setOf` `Real.instLT` `Norm.norm` `NormedAddCommGroup.toNorm` `Filter.atTop` `Real.instPreorder` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	`IsTightMeasureSet` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`isTightMeasureSet_of_tendsto_measure_compl_closedBall` `iSup_congr_Prop` `Set.ext` `dist_zero_right`
`isTightMeasureSet_range_iff_tendsto_limsup_inner` 📖	mathematical	`IsFiniteMeasure`	`IsTightMeasureSet` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.range` `Measure` `Filter.Tendsto` `Real` `ENNReal` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `DFunLike.coe` `Set` `Measure.instFunLike` `setOf` `Real.instLT` `Norm.norm` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Inner.inner` `InnerProductSpace.toInner` `Filter.atTop` `Nat.instPreorder` `Real.instPreorder` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`tendsto_of_tendsto_of_tendsto_of_le_of_le` `ENNReal.instOrderTopology` `tendsto_const_nhds` `isTightMeasureSet_iff_inner_tendsto` `zero_le` `ENNReal.instCanonicallyOrderedAdd` `iSup_range` `Filter.limsup_le_iSup` `isTightMeasureSet_range_of_tendsto_limsup_inner`
`isTightMeasureSet_range_iff_tendsto_limsup_measure_norm_gt` 📖	mathematical	`IsFiniteMeasure`	`IsTightMeasureSet` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.range` `Measure` `Filter.Tendsto` `Real` `ENNReal` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `DFunLike.coe` `Set` `Measure.instFunLike` `setOf` `Real.instLT` `Norm.norm` `NormedAddCommGroup.toNorm` `Filter.atTop` `Nat.instPreorder` `Real.instPreorder` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`tendsto_measure_norm_gt_of_isTightMeasureSet` `tendsto_of_tendsto_of_tendsto_of_le_of_le` `ENNReal.instOrderTopology` `tendsto_const_nhds` `zero_le` `ENNReal.instCanonicallyOrderedAdd` `iSup_range` `Filter.limsup_le_iSup` `isTightMeasureSet_range_of_tendsto_limsup_measure_norm_gt`
`isTightMeasureSet_range_of_tendsto_limsup_inner` 📖	mathematical	`IsFiniteMeasure` `Filter.Tendsto` `Real` `ENNReal` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `setOf` `Real.instLT` `Norm.norm` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.atTop` `Nat.instPreorder` `Real.instPreorder` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	`IsTightMeasureSet` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.range` `Measure`	—	`isTightMeasureSet_of_inner_tendsto` `iSup_range` `Nat.tendsto_iSup_of_tendsto_limsup` `ENNReal.instOrderTopology` `isTightMeasureSet_singleton` `TopologicalSpace.IsCompletelyMetrizableSpace.toIsCompletelyPseudoMetrizableSpace` `TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable` `RCLike.toCompleteSpace` `EMetric.instIsCountablyGeneratedUniformity` `T6Space.toT0Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `secondCountable_of_proper` `FiniteDimensional.proper_real` `FiniteDimensional.rclike_to_real` `RCLike.borelSpace` `Measure.isFiniteMeasure_map` `Measure.map_apply` `Continuous.measurable` `BorelSpace.opensMeasurable` `Continuous.inner` `continuous_const` `continuous_id'` `MeasurableSet.preimage` `measurableSet_Ioi` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Measurable.norm` `measurable_id'` `iSup_congr_Prop` `iSup_iSup_eq_left` `isTightMeasureSet_iff_tendsto_measure_norm_gt` `measure_mono` `Measure.instOuterMeasureClass` `Set.setOf_subset_setOf_of_imp` `lt_imp_lt_of_le_of_le` `le_refl`
`isTightMeasureSet_range_of_tendsto_limsup_inner_of_norm_eq_one` 📖	mathematical	`IsFiniteMeasure` `Filter.Tendsto` `Real` `ENNReal` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `setOf` `Real.instLT` `Norm.norm` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.atTop` `Nat.instPreorder` `Real.instPreorder` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	`IsTightMeasureSet` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.range` `Measure`	—	`isTightMeasureSet_range_of_tendsto_limsup_inner` `inner_zero_left` `Filter.tendsto_congr'` `Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `norm_zero` `not_lt` `measure_empty` `Measure.instOuterMeasureClass` `Filter.limsup_const` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `tendsto_const_nhds` `Filter.Tendsto.comp` `norm_smul` `NormedSpace.toNormSMulClass` `norm_inv` `norm_algebraMap'` `NormedDivisionRing.to_normOneClass` `abs_norm` `inv_mul_cancel₀` `ne_of_gt` `norm_pos_iff` `Filter.tendsto_const_mul_atTop_of_pos` `Real.instIsStrictOrderedRing` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Filter.tendsto_id` `inner_smul_left` `map_inv₀` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `RCLike.conj_ofReal` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_norm` `mul_lt_mul_iff_right₀`
`isTightMeasureSet_range_of_tendsto_limsup_measureReal_inner_of_norm_eq_one` 📖	mathematical	`IsFiniteMeasure` `Filter.Tendsto` `Real` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Real.instConditionallyCompleteLinearOrder` `Measure.real` `setOf` `Real.instLT` `Norm.norm` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filter.atTop` `Nat.instPreorder` `Real.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `Filter.Eventually` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Set.univ` `ENNReal.ofNNReal`	`IsTightMeasureSet` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.range` `Measure`	—	`isTightMeasureSet_range_of_tendsto_limsup_inner_of_norm_eq_one` `ENNReal.ofReal_limsup_toReal` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.mp_mem` `Filter.univ_mem'` `LE.le.trans` `measure_mono` `Measure.instOuterMeasureClass` `Set.subset_univ` `ENNReal.tendsto_ofReal`
`isTightMeasureSet_range_of_tendsto_limsup_measure_norm_gt` 📖	mathematical	`IsFiniteMeasure` `Filter.Tendsto` `Real` `ENNReal` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `setOf` `Real.instLT` `Norm.norm` `NormedAddCommGroup.toNorm` `Filter.atTop` `Nat.instPreorder` `Real.instPreorder` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	`IsTightMeasureSet` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.range` `Measure`	—	`iSup_range` `Nat.tendsto_iSup_of_tendsto_limsup` `ENNReal.instOrderTopology` `isTightMeasureSet_singleton` `TopologicalSpace.IsCompletelyMetrizableSpace.toIsCompletelyPseudoMetrizableSpace` `TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable` `complete_of_proper` `EMetric.instIsCountablyGeneratedUniformity` `T6Space.toT0Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `secondCountable_of_proper` `iSup_congr_Prop` `iSup_iSup_eq_left` `isTightMeasureSet_iff_tendsto_measure_norm_gt` `measure_mono` `Measure.instOuterMeasureClass` `Set.setOf_subset_setOf_of_imp` `lt_imp_lt_of_le_of_le` `le_refl`
`tendsto_measure_compl_closedBall_of_isTightMeasureSet` 📖	mathematical	`IsTightMeasureSet` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	`Filter.Tendsto` `Real` `ENNReal` `iSup` `Measure` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set` `Set.instMembership` `DFunLike.coe` `Measure.instFunLike` `Compl.compl` `Set.instCompl` `Metric.closedBall` `Filter.atTop` `Real.instPreorder` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`Filter.Tendsto.comp` `Filter.Tendsto.mono_right` `Filter.HasAntitoneBasis.tendsto_smallSets` `Metric.hasAntitoneBasis_cobounded_compl_closedBall` `Filter.monotone_smallSets` `Metric.cobounded_le_cocompact` `iSup_apply`
`tendsto_measure_norm_gt_of_isTightMeasureSet` 📖	mathematical	`IsTightMeasureSet` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Filter.Tendsto` `Real` `ENNReal` `iSup` `Measure` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set` `Set.instMembership` `DFunLike.coe` `Measure.instFunLike` `setOf` `Real.instLT` `Norm.norm` `NormedAddCommGroup.toNorm` `Filter.atTop` `Real.instPreorder` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`tendsto_measure_compl_closedBall_of_isTightMeasureSet` `iSup_congr_Prop` `Set.ext` `dist_zero_right`

---

← Back to Index