Documentation Verification Report

Tight

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

Statistics

Metric	Count
Definitions `IsTightMeasureSet`	1
Theorems `inter`, `map`, `of_compactSpace`, `subset`, `union`, `IsTightMeasureSet_iff_exists_isCompact_measure_compl_le`, `exists_measure_iUnion_gt_of_isCompact_closure`, `isTightMeasureSet_iff_exists_isCompact_measure_compl_le`, `isTightMeasureSet_of_isCompact_closure`, `isTightMeasureSet_singleton`, `isTightMeasureSet_singleton_of_innerRegular`, `isTightMeasureSet_singleton_of_innerRegularWRT`	12
Total	13

MeasureTheory

Definitions

Name	Category	Theorems
`IsTightMeasureSet` 📖	MathDef	25 math math: `isTightMeasureSet_of_tendsto_measure_norm_gt`, `isTightMeasureSet_range_of_tendsto_limsup_measureReal_inner_of_norm_eq_one`, `isTightMeasureSet_iff_inner_tendsto`, `IsTightMeasureSet.union`, `isTightMeasureSet_singleton_of_innerRegularWRT`, `IsTightMeasureSet.subset`, `isTightMeasureSet_range_of_tendsto_limsup_inner_of_norm_eq_one`, `IsTightMeasureSet.inter`, `isTightMeasureSet_of_tendsto_measure_compl_closedBall`, `isTightMeasureSet_range_of_tendsto_limsup_inner`, `isTightMeasureSet_range_iff_tendsto_limsup_inner`, `isTightMeasureSet_of_tendsto_charFun`, `isTightMeasureSet_singleton`, `IsTightMeasureSet.map`, `isTightMeasureSet_of_isCompact_closure`, `isTightMeasureSet_of_inner_tendsto`, `isTightMeasureSet_iff_exists_isCompact_measure_compl_le`, `isTightMeasureSet_range_of_tendsto_limsup_measure_norm_gt`, `IsTightMeasureSet_iff_exists_isCompact_measure_compl_le`, `isTightMeasureSet_iff_tendsto_measure_norm_gt`, `isTightMeasureSet_singleton_of_innerRegular`, `isTightMeasureSet_range_iff_tendsto_limsup_measure_norm_gt`, `IsTightMeasureSet.of_compactSpace`, `isTightMeasureSet_iff_tendsto_measure_compl_closedBall`, `isTightMeasureSet_of_forall_basis_tendsto`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`IsTightMeasureSet_iff_exists_isCompact_measure_compl_le` 📖	mathematical	—	`IsTightMeasureSet` `Set` `IsCompact` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `Measure` `Measure.instFunLike` `Compl.compl` `Set.instCompl`	—	`isTightMeasureSet_iff_exists_isCompact_measure_compl_le`
`exists_measure_iUnion_gt_of_isCompact_closure` 📖	mathematical	`IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Set.iUnion` `Set.univ` `IsCompact` `ProbabilityMeasure` `ProbabilityMeasure.instTopologicalSpace` `closure` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `Preorder.toLE` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.instSub` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ENNReal.ofNNReal` `DFunLike.coe` `ProbabilityMeasure` `Set` `NNReal` `ProbabilityMeasure.instFunLike` `Set.iUnion`	—	`ne_top_of_le_ne_top` `CanLift.prf` `ENNReal.canLift` `IsCompact.isSeqCompact` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `instPseudoMetrizableSpaceProbabilityMeasureOfSeparableSpace` `PseudoEMetricSpace.pseudoMetrizableSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `subset_closure` `isOpen_biUnion` `ProbabilityMeasure.le_liminf_measure_open_of_tendsto` `instHasOuterApproxClosedOfPseudoMetrizableSpace` `NNReal.toReal_liminf` `ENNReal.ofNNReal_liminf` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `LE.le.trans` `instReflLe` `ProbabilityMeasure.apply_le_one` `Filter.liminf_le_liminf` `ProbabilityMeasure.apply_mono` `Set.biUnion_mono` `le_trans` `StrictMono.le_apply` `instWellFoundedLTNat` `le_rfl` `Filter.liminf_le_of_le` `ENNReal.ofReal_le_ofReal_iff` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `ENNReal.ofReal_coe_nnreal` `Nat.cast_one` `le_refl` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat` `Nat.instAtLeastTwoHAddOfNat` `Filter.Tendsto.eventually_const_le` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instIsOrderedRing` `Real.instNontrivial` `NNReal.tendsto_coe` `ProbabilityMeasure.coeFn_univ` `Filter.mp_mem` `Filter.univ_mem'` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `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.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Mathlib.Tactic.CancelDenoms.sub_subst` `Mathlib.Tactic.CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Meta.NormNum.isNat_lt_true` `Filter.Eventually.exists` `Filter.atTop_neBot` `Mathlib.Tactic.Push.not_forall_eq`
`isTightMeasureSet_iff_exists_isCompact_measure_compl_le` 📖	mathematical	—	`IsTightMeasureSet` `Set` `IsCompact` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `Measure` `Measure.instFunLike` `Compl.compl` `Set.instCompl`	—	`ENNReal.tendsto_nhds` `ENNReal.zero_ne_top` `zero_add` `iSup_apply` `ENNReal.instOrderedSub` `ENNReal.instCanonicallyOrderedAdd` `subset_rfl` `Set.instReflSubset` `LE.le.trans` `OuterMeasure.mono`
`isTightMeasureSet_of_isCompact_closure` 📖	mathematical	`IsCompact` `ProbabilityMeasure` `ProbabilityMeasure.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `closure`	`IsTightMeasureSet` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `setOf` `Measure` `ProbabilityMeasure` `Set` `Set.instMembership` `ProbabilityMeasure.toMeasure`	—	`isTightMeasureSet_iff_exists_isCompact_measure_compl_le` `isEmpty_or_nonempty` `isCompact_empty` `Set.compl_empty` `Set.univ_eq_empty_iff` `measure_empty` `Measure.instOuterMeasureClass` `ENNReal.instCanonicallyOrderedAdd` `TopologicalSpace.exists_dense_seq` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `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` `Set.ext` `Set.mem_iUnion` `Metric.denseRange_iff` `lt_or_ge` `IsProbabilityMeasure.measure_univ` `ProbabilityMeasure.instIsProbabilityMeasureToMeasure` `le_of_lt` `Nat.instAtLeastTwoHAddOfNat` `exists_measure_iUnion_gt_of_isCompact_closure` `Metric.isOpen_ball` `ENNReal.instNoZeroDivisors` `ENNReal.zpow_pos` `ENNReal.instCharZero` `Left.mul_le_one` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `ENNReal.zpow_le_one_of_nonpos` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_add` `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.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing` `Mathlib.Tactic.Linarith.natCast_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `Set.compl_iInter` `Set.compl_iUnion` `measure_iUnion_le` `instCountableNat` `measure_compl` `MeasurableSet.iUnion` `Prop.countable` `measurableSet_closure` `IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `ENNReal.tsum_le_tsum` `tsub_le_iff_tsub_le` `ENNReal.instOrderedSub` `LT.lt.le` `neg_add_rev` `le_imp_le_of_le_of_le` `Nat.cast_add` `Nat.cast_one` `le_refl` `add_le_add_left` `covariant_swap_add_of_covariant_add` `ENNReal.coe_le_coe_of_le` `ProbabilityMeasure.apply_mono` `Set.iUnion_mono''` `Mathlib.Tactic.GCongr.rel_imp_rel` `Set.instIsTransSubset` `subset_refl` `Set.instReflSubset` `subset_closure` `Metric.ball_subset_ball` `StrictAnti.antitone` `ENNReal.tsum_mul_left` `mul_one` `Mathlib.Tactic.Ring.atom_pf'` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.RingNF.add_assoc_rev` `Mathlib.Tactic.RingNF.int_rawCast_neg` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `Mathlib.Tactic.RingNF.mul_neg` `Mathlib.Tactic.RingNF.add_neg` `add_zero` `ENNReal.tsum_two_zpow_neg_add_one` `TotallyBounded.isCompact_of_isClosed` `Metric.totallyBounded_iff` `Filter.Eventually.exists` `Filter.atTop_neBot` `instIsDirectedOrder` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.Tendsto.eventually_lt_const` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Set.Finite.image` `Set.finite_Iic` `Set.iUnion_congr_Prop` `Set.iUnion_exists` `Set.biUnion_and'` `Set.iUnion_iUnion_eq_right` `Set.iInter_subset` `HasSubset.Subset.trans` `Metric.closure_ball_subset_closedBall` `Metric.closedBall_subset_ball` `isClosed_iInter` `Set.Finite.isClosed_biUnion` `isClosed_closure`
`isTightMeasureSet_singleton` 📖	mathematical	—	`IsTightMeasureSet` `Measure` `Set` `Set.instSingletonSet`	—	`isTightMeasureSet_singleton_of_innerRegularWRT` `BorelSpace.opensMeasurable` `innerRegular_isCompact_isClosed_measurableSet_of_finite`
`isTightMeasureSet_singleton_of_innerRegular` 📖	mathematical	—	`IsTightMeasureSet` `Measure` `Set` `Set.instSingletonSet`	—	`isTightMeasureSet_singleton_of_innerRegularWRT` `Measure.InnerRegular.innerRegular` `IsCompact.isClosed`
`isTightMeasureSet_singleton_of_innerRegularWRT` 📖	mathematical	`Measure.InnerRegularWRT` `IsCompact` `IsClosed` `MeasurableSet`	`IsTightMeasureSet` `Measure` `Set` `Set.instSingletonSet`	—	`isTightMeasureSet_iff_exists_isCompact_measure_compl_le` `lt_or_ge` `ENNReal.sub_lt_self` `measure_ne_top` `LT.lt.ne_bot` `LT.lt.ne'` `MeasurableSet.univ` `measure_compl` `IsClosed.measurableSet` `tsub_le_iff_right` `ENNReal.instOrderedSub` `LT.lt.le` `add_comm` `ENNReal.sub_lt_iff_lt_right` `ne_top_of_lt` `isCompact_empty` `Set.compl_empty`

MeasureTheory.IsTightMeasureSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inter` 📖	mathematical	`MeasureTheory.IsTightMeasureSet`	`MeasureTheory.IsTightMeasureSet` `Set` `MeasureTheory.Measure` `Set.instInter`	—	`subset` `Set.inter_subset_left`
`map` 📖	mathematical	`MeasureTheory.IsTightMeasureSet` `Continuous`	`MeasureTheory.IsTightMeasureSet` `Set.image` `MeasureTheory.Measure` `MeasureTheory.Measure.map`	—	`MeasureTheory.isTightMeasureSet_iff_exists_isCompact_measure_compl_le` `IsCompact.image` `MeasureTheory.Measure.map_apply_of_aemeasurable` `MeasurableSet.compl` `IsCompact.measurableSet` `LE.le.trans` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.subset_preimage_image` `MeasureTheory.Measure.map_of_not_aemeasurable` `ENNReal.instCanonicallyOrderedAdd`
`of_compactSpace` 📖	mathematical	—	`MeasureTheory.IsTightMeasureSet`	—	`Filter.cocompact_eq_bot` `Filter.smallSets_bot` `iSup_apply` `iSup_congr_Prop` `MeasureTheory.measure_empty` `MeasureTheory.Measure.instOuterMeasureClass` `ENNReal.iSup_zero` `ciSup_const` `mem_of_mem_nhds`
`subset` 📖	mathematical	`MeasureTheory.IsTightMeasureSet` `Set` `MeasureTheory.Measure` `Set.instHasSubset`	`MeasureTheory.IsTightMeasureSet`	—	`tendsto_of_tendsto_of_tendsto_of_le_of_le` `ENNReal.instOrderTopology` `tendsto_const_nhds` `iSup_apply` `ENNReal.instCanonicallyOrderedAdd` `iSup_le_iSup_of_subset`
`union` 📖	mathematical	`MeasureTheory.IsTightMeasureSet`	`MeasureTheory.IsTightMeasureSet` `Set` `MeasureTheory.Measure` `Set.instUnion`	—	`eq_1` `iSup_union` `max_self` `Filter.Tendsto.sup_nhds` `TopologicalLattice.toContinuousSup` `LinearOrder.topologicalLattice` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology`

---

← Back to Index