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, tendsto_measure_compl_closedBall_of_isTightMeasureSet, tendsto_measure_norm_gt_of_isTightMeasureSet	9
Total	9

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 CompletePartialOrder.toSupSet CompleteLattice.toCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice 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 CompletePartialOrder.toSupSet CompleteLattice.toCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice 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 CompletePartialOrder.toSupSet CompleteLattice.toCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice 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 CompletePartialOrder.toSupSet CompleteLattice.toCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice 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	—	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 Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Fintype.card_pos ciSup_le measure_iUnion_fintype_le iSup_le Finset.sum_le_sum 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 CompletePartialOrder.toSupSet CompleteLattice.toCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice 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	—	isTightMeasureSet_of_forall_basis_tendsto
isTightMeasureSet_of_tendsto_measure_compl_closedBall 📖	mathematical	Filter.Tendsto Real ENNReal iSup Measure CompletePartialOrder.toSupSet CompleteLattice.toCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice 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 CompletePartialOrder.toSupSet CompleteLattice.toCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice 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
tendsto_measure_compl_closedBall_of_isTightMeasureSet 📖	mathematical	IsTightMeasureSet UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	Filter.Tendsto Real ENNReal iSup Measure CompletePartialOrder.toSupSet CompleteLattice.toCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice 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 CompletePartialOrder.toSupSet CompleteLattice.toCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice 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