Documentation Verification Report

RegularityCompacts

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

Statistics

Metric	Count
Definitions	0
Theorems `innerRegular_isCompact_isClosed_measurableSet`, `exists_isCompact_closure_measure_compl_lt`, `innerRegularWRT_isCompact`, `innerRegularWRT_isCompact_closure`, `innerRegularWRT_isCompact_closure_iff`, `innerRegularWRT_isCompact_closure_of_univ`, `innerRegularWRT_isCompact_isClosed`, `innerRegularWRT_isCompact_isClosed_iff`, `innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure`, `innerRegularWRT_isCompact_isClosed_isOpen`, `innerRegularWRT_isCompact_isOpen`, `innerRegularWRT_of_exists_compl_lt`, `innerRegular_isCompact_isClosed_measurableSet_of_finite`, `instInnerRegularCompactLTTopOfIsCompletelyPseudoMetrizableSpace`, `instInnerRegularOfIsCompletelyPseudoMetrizableSpace`	15
Total	15

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isCompact_closure_measure_compl_lt` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal`	`IsCompact` `closure` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Compl.compl` `Set.instCompl`	—	`isEmpty_or_nonempty` `IsClosed.closure_eq` `Finite.instDiscreteTopology` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `TopologicalSpace.IsCompletelyMetrizableSpace.MetrizableSpace` `PolishSpace.toIsCompletelyMetrizableSpace` `instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable` `TopologicalSpace.UpgradedIsCompletelyPseudoMetrizableSpace.toCompleteSpace` `EMetric.instIsCountablyGeneratedUniformity` `T6Space.toT0Space` `TopologicalSpace.DiscreteTopology.metrizableSpace` `Subsingleton.discreteTopology` `IsEmpty.instSubsingleton` `Finite.of_subsingleton` `Set.eq_empty_of_isEmpty` `instIsEmptySubtype` `measure_empty` `Measure.instOuterMeasureClass` `TopologicalSpace.denseRange_denseSeq` `Filter.HasBasis.exists_antitone_subbasis` `uniformity_hasBasis_open_symmetric` `DenseRange.iUnion_uniformity_ball` `exists_measure_iInter_lt` `instCountableNat` `MeasurableSet.nullMeasurableSet` `MeasurableSet.compl` `measurable_prodMk_left` `IsOpen.measurableSet` `Prod.opensMeasurableSpace` `secondCountableTopologyEither_of_right` `measure_ne_top` `Set.compl_iUnion` `Set.compl_univ` `ENNReal.exists_pos_sum_of_countable'` `ne_of_gt` `isCompact_closure_interUnionBalls` `Filter.HasAntitoneBasis.toHasBasis` `interUnionBalls.eq_1` `Set.compl_iInter` `LE.le.trans_lt` `LE.le.trans` `measure_iUnion_le` `ENNReal.tsum_le_tsum` `Set.ext` `SetRel.comm` `Set.iUnion_congr_Prop` `LT.lt.le` `Function.sometimes_spec`
`innerRegularWRT_isCompact` 📖	mathematical	—	`Measure.InnerRegularWRT` `IsCompact` `IsClosed`	—	`innerRegularWRT_isCompact_closure_iff` `instR1Space` `TopologicalSpace.PseudoMetrizableSpace.regularSpace` `TopologicalSpace.IsCompletelyPseudoMetrizableSpace.PseudoMetrizableSpace` `innerRegularWRT_isCompact_closure`
`innerRegularWRT_isCompact_closure` 📖	mathematical	—	`Measure.InnerRegularWRT` `Set` `IsCompact` `closure` `IsClosed`	—	`innerRegularWRT_isCompact_closure_of_univ` `exists_isCompact_closure_measure_compl_lt`
`innerRegularWRT_isCompact_closure_iff` 📖	mathematical	—	`Measure.InnerRegularWRT` `Set` `IsCompact` `closure` `IsClosed`	—	`closure_minimal` `LT.lt.trans_le` `measure_mono` `Measure.instOuterMeasureClass` `subset_closure` `closure_closure` `IsCompact.closure`
`innerRegularWRT_isCompact_closure_of_univ` 📖	mathematical	`IsCompact` `closure` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Compl.compl` `Set.instCompl`	`Measure.InnerRegularWRT` `IsClosed`	—	`innerRegularWRT_of_exists_compl_lt` `IsCompact.inter_right` `IsCompact.of_isClosed_subset` `isClosed_closure` `LE.le.trans_eq` `closure_inter_subset_inter_closure` `IsClosed.closure_eq`
`innerRegularWRT_isCompact_isClosed` 📖	mathematical	—	`Measure.InnerRegularWRT` `IsCompact` `IsClosed`	—	`innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure` `instR1Space` `TopologicalSpace.PseudoMetrizableSpace.regularSpace` `TopologicalSpace.IsCompletelyPseudoMetrizableSpace.PseudoMetrizableSpace` `innerRegularWRT_isCompact_closure`
`innerRegularWRT_isCompact_isClosed_iff` 📖	mathematical	—	`Measure.InnerRegularWRT` `IsCompact` `IsClosed`	—	`innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure` `innerRegularWRT_isCompact_closure_iff`
`innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure` 📖	mathematical	—	`Measure.InnerRegularWRT` `IsCompact` `IsClosed` `Set` `closure`	—	`IsCompact.closure` `closure_minimal` `LT.lt.trans_le` `measure_mono` `Measure.instOuterMeasureClass` `subset_closure`
`innerRegularWRT_isCompact_isClosed_isOpen` 📖	mathematical	—	`Measure.InnerRegularWRT` `IsCompact` `IsClosed` `IsOpen`	—	`Measure.InnerRegularWRT.trans` `innerRegularWRT_isCompact_isClosed` `Measure.InnerRegularWRT.of_pseudoMetrizableSpace` `TopologicalSpace.IsCompletelyPseudoMetrizableSpace.PseudoMetrizableSpace`
`innerRegularWRT_isCompact_isOpen` 📖	mathematical	—	`Measure.InnerRegularWRT` `IsCompact` `IsOpen`	—	`Measure.InnerRegularWRT.trans` `innerRegularWRT_isCompact` `Measure.InnerRegularWRT.of_pseudoMetrizableSpace` `TopologicalSpace.IsCompletelyPseudoMetrizableSpace.PseudoMetrizableSpace`
`innerRegularWRT_of_exists_compl_lt` 📖	mathematical	`Set` `Set.instInter` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `Measure` `Measure.instFunLike` `Compl.compl` `Set.instCompl`	`Measure.InnerRegularWRT`	—	`tsub_pos_of_lt` `ENNReal.instCanonicallyOrderedAdd` `ENNReal.instOrderedSub` `Set.inter_subset_right` `LE.le.trans_lt` `measure_mono` `Measure.instOuterMeasureClass` `Set.diff_inter_self_eq_diff` `le_measure_diff` `lt_of_tsub_lt_tsub_left` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid`
`innerRegular_isCompact_isClosed_measurableSet_of_finite` 📖	mathematical	—	`Measure.InnerRegularWRT` `IsCompact` `IsClosed` `MeasurableSet`	—	`Measure.InnerRegularWRT.measurableSet_of_isOpen` `Measure.WeaklyRegular.toOuterRegular` `Measure.WeaklyRegular.of_pseudoMetrizableSpace_secondCountable_of_locallyFinite` `TopologicalSpace.IsCompletelyPseudoMetrizableSpace.PseudoMetrizableSpace` `IsFiniteMeasure.toIsLocallyFiniteMeasure` `innerRegularWRT_isCompact_isClosed_isOpen` `BorelSpace.opensMeasurable` `Set.diff_eq` `IsCompact.inter_right` `IsOpen.isClosed_compl` `IsClosed.inter` `isClosed_compl_iff` `measure_ne_top`
`instInnerRegularCompactLTTopOfIsCompletelyPseudoMetrizableSpace` 📖	mathematical	—	`Measure.InnerRegularCompactLTTop`	—	`Ne.lt_top` `Measure.restrict_apply_self` `MeasurableSet.exists_lt_isCompact_of_ne_top` `Measure.InnerRegular.instInnerRegularCompactLTTop` `instInnerRegularOfIsCompletelyPseudoMetrizableSpace` `Restrict.isFiniteMeasure` `Measure.restrict_eq_self`
`instInnerRegularOfIsCompletelyPseudoMetrizableSpace` 📖	mathematical	—	`Measure.InnerRegular`	—	`Measure.InnerRegularWRT.measurableSet_of_isOpen` `Measure.WeaklyRegular.toOuterRegular` `Measure.WeaklyRegular.of_pseudoMetrizableSpace_secondCountable_of_locallyFinite` `TopologicalSpace.IsCompletelyPseudoMetrizableSpace.PseudoMetrizableSpace` `IsFiniteMeasure.toIsLocallyFiniteMeasure` `innerRegularWRT_isCompact_isOpen` `BorelSpace.opensMeasurable` `IsCompact.inter_right` `IsOpen.isClosed_compl` `Measure.InnerRegularCompactLTTop.instInnerRegularOfSigmaFinite` `sigmaFinite_of_locallyFinite`

MeasureTheory.PolishSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`innerRegular_isCompact_isClosed_measurableSet` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegularWRT` `IsCompact` `IsClosed` `MeasurableSet`	—	`MeasureTheory.innerRegular_isCompact_isClosed_measurableSet_of_finite`

---

← Back to Index