Documentation Verification Report

MeasuredSets

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

Statistics

Metric	Count
Definitions `MeasuredSets`, `instPseudoEMetricSpaceMeasuredSets`, `instPseudoMetricSpaceMeasuredSetsOfIsFiniteMeasure`, `instSetLikeMeasuredSets`	4
Theorems `continuous_measure`, `dist_def`, `edist_def`, `lipschitzWith_measureReal`, `real_sub_real_le_dist`, `sub_le_edist`, `dense_of_generateFrom_isSetRing`, `dense_of_generateFrom_isSetSemiring`, `exists_measure_symmDiff_lt_of_generateFrom_isSetRing`, `exists_measure_symmDiff_lt_of_generateFrom_isSetSemiring`	10
Total	14

MeasureTheory

Definitions

Name	Category	Theorems
`MeasuredSets` 📖	CompOp	8 math math: `MeasuredSets.real_sub_real_le_dist`, `MeasuredSets.sub_le_edist`, `dense_of_generateFrom_isSetRing`, `dense_of_generateFrom_isSetSemiring`, `MeasuredSets.lipschitzWith_measureReal`, `MeasuredSets.dist_def`, `MeasuredSets.continuous_measure`, `MeasuredSets.edist_def`
`instPseudoEMetricSpaceMeasuredSets` 📖	CompOp	4 math math: `MeasuredSets.sub_le_edist`, `MeasuredSets.lipschitzWith_measureReal`, `MeasuredSets.continuous_measure`, `MeasuredSets.edist_def`
`instPseudoMetricSpaceMeasuredSetsOfIsFiniteMeasure` 📖	CompOp	4 math math: `MeasuredSets.real_sub_real_le_dist`, `dense_of_generateFrom_isSetRing`, `dense_of_generateFrom_isSetSemiring`, `MeasuredSets.dist_def`
`instSetLikeMeasuredSets` 📖	CompOp	8 math math: `MeasuredSets.real_sub_real_le_dist`, `MeasuredSets.sub_le_edist`, `dense_of_generateFrom_isSetRing`, `dense_of_generateFrom_isSetSemiring`, `MeasuredSets.lipschitzWith_measureReal`, `MeasuredSets.dist_def`, `MeasuredSets.continuous_measure`, `MeasuredSets.edist_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dense_of_generateFrom_isSetRing` 📖	mathematical	`IsSetRing` `Set` `Set.Countable` `Set.instHasSubset` `DFunLike.coe` `Measure` `ENNReal` `Measure.instFunLike` `Compl.compl` `Set.instCompl` `Set.sUnion` `instZeroENNReal` `MeasurableSpace.generateFrom`	`Dense` `MeasuredSets` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpaceMeasuredSetsOfIsFiniteMeasure` `Set.preimage` `Set` `SetLike.coe` `instSetLikeMeasuredSets`	—	`EMetric.dense_iff` `exists_measure_symmDiff_lt_of_generateFrom_isSetRing` `MeasurableSpace.measurableSet_generateFrom`
`dense_of_generateFrom_isSetSemiring` 📖	mathematical	`IsSetSemiring` `Set` `Set.Countable` `Set.instHasSubset` `DFunLike.coe` `Measure` `ENNReal` `Measure.instFunLike` `Compl.compl` `Set.instCompl` `Set.sUnion` `instZeroENNReal` `MeasurableSpace.generateFrom`	`Dense` `MeasuredSets` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `instPseudoMetricSpaceMeasuredSetsOfIsFiniteMeasure` `Set.preimage` `Set` `SetLike.coe` `instSetLikeMeasuredSets` `DFunLike.coe` `ClosureOperator` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `supClosure` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice`	—	`EMetric.dense_iff` `exists_measure_symmDiff_lt_of_generateFrom_isSetSemiring` `measurableSet_generateFrom_of_mem_supClosure`
`exists_measure_symmDiff_lt_of_generateFrom_isSetRing` 📖	mathematical	`IsSetRing` `Set` `Set.Countable` `Set.instHasSubset` `DFunLike.coe` `Measure` `ENNReal` `Measure.instFunLike` `Compl.compl` `Set.instCompl` `Set.sUnion` `instZeroENNReal` `MeasurableSpace.generateFrom` `MeasurableSet` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder`	`Set` `Set.instMembership` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `Measure` `Measure.instFunLike` `symmDiff` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.instSDiff`	—	`MeasurableSpace.induction_on_inter` `IsSetSemiring.isPiSystem` `IsSetRing.isSetSemiring` `IsSetRing.empty_mem` `symmDiff_self` `measure_empty` `Measure.instOuterMeasureClass` `Nat.instAtLeastTwoHAddOfNat` `ENNReal.half_pos` `LT.lt.ne'` `Set.Countable.union` `Set.union_singleton` `Set.sUnion_insert` `Set.empty_union` `Set.Countable.exists_eq_range` `IsSetRing.accumulate_mem` `Set.iUnion_accumulate` `Set.compl_iUnion` `tendsto_measure_iInter_atTop` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat` `PseudoEMetricSpace.pseudoMetrizableSpace` `MeasurableSet.nullMeasurableSet` `MeasurableSet.compl` `MeasurableSpace.measurableSet_generateFrom` `Set.monotone_accumulate` `Set.accumulate_zero_nat` `Filter.Eventually.exists` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `tendsto_order` `ENNReal.instOrderTopology` `IsSetRing.diff_mem` `measure_mono` `measure_union_le` `WithTop.add_lt_add` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `NNReal.addLeftMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `NNReal.addLeftReflectLT` `covariant_swap_add_of_covariant_add` `ENNReal.add_halves` `ENNReal.exists_pos_sum_of_countable'` `tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint` `IsSetRing.biUnion_mem` `Set.iUnion_congr_Prop` `LE.le.trans` `add_le_add_left` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `measure_biUnion_finset_le` `Finset.sum_le_sum` `LT.lt.le` `ENNReal.sum_le_tsum`
`exists_measure_symmDiff_lt_of_generateFrom_isSetSemiring` 📖	mathematical	`IsSetSemiring` `Set` `Set.Countable` `Set.instHasSubset` `DFunLike.coe` `Measure` `ENNReal` `Measure.instFunLike` `Compl.compl` `Set.instCompl` `Set.sUnion` `instZeroENNReal` `MeasurableSpace.generateFrom` `MeasurableSet` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder`	`Set` `Set.instMembership` `DFunLike.coe` `ClosureOperator` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `supClosure` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ENNReal` `Preorder.toLT` `ENNReal.instPartialOrder` `Measure` `Measure.instFunLike` `symmDiff` `SemilatticeSup.toMax` `Set.instSDiff`	—	`exists_measure_symmDiff_lt_of_generateFrom_isSetRing` `IsSetSemiring.isSetRing_supClosure` `HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_supClosure` `le_antisymm` `MeasurableSpace.generateFrom_mono` `MeasurableSpace.generateFrom_le` `measurableSet_generateFrom_of_mem_supClosure`

MeasureTheory.MeasuredSets

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_measure` 📖	mathematical	—	`Continuous` `MeasureTheory.MeasuredSets` `ENNReal` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `MeasureTheory.instPseudoEMetricSpaceMeasuredSets` `ENNReal.instTopologicalSpace` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `SetLike.coe` `MeasureTheory.instSetLikeMeasuredSets`	—	`continuous_of_le_add_edist` `ENNReal.one_ne_top` `one_mul` `tsub_le_iff_left` `ENNReal.instOrderedSub` `sub_le_edist`
`dist_def` 📖	mathematical	—	`Dist.dist` `MeasureTheory.MeasuredSets` `PseudoMetricSpace.toDist` `MeasureTheory.instPseudoMetricSpaceMeasuredSetsOfIsFiniteMeasure` `MeasureTheory.Measure.real` `symmDiff` `Set` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.instSDiff` `SetLike.coe` `MeasureTheory.instSetLikeMeasuredSets`	—	—
`edist_def` 📖	mathematical	—	`EDist.edist` `MeasureTheory.MeasuredSets` `PseudoEMetricSpace.toEDist` `MeasureTheory.instPseudoEMetricSpaceMeasuredSets` `DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `symmDiff` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.instSDiff` `SetLike.coe` `MeasureTheory.instSetLikeMeasuredSets`	—	—
`lipschitzWith_measureReal` 📖	mathematical	—	`LipschitzWith` `MeasureTheory.MeasuredSets` `Real` `MeasureTheory.instPseudoEMetricSpaceMeasuredSets` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `Real.metricSpace` `NNReal` `NNReal.instOne` `MeasureTheory.Measure.real` `SetLike.coe` `MeasureTheory.instSetLikeMeasuredSets`	—	`LipschitzWith.of_le_add` `sub_le_iff_le_add'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `real_sub_real_le_dist`
`real_sub_real_le_dist` 📖	mathematical	—	`Real` `Real.instLE` `Real.instSub` `MeasureTheory.Measure.real` `SetLike.coe` `MeasureTheory.MeasuredSets` `MeasureTheory.instSetLikeMeasuredSets` `Dist.dist` `PseudoMetricSpace.toDist` `MeasureTheory.instPseudoMetricSpaceMeasuredSetsOfIsFiniteMeasure`	—	`dist_edist` `le_imp_le_of_le_of_le` `le_refl` `ENNReal.toReal_mono` `edist_ne_top` `sub_le_edist` `ENNReal.le_toReal_sub` `MeasureTheory.measure_ne_top`
`sub_le_edist` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.instSub` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `SetLike.coe` `MeasureTheory.MeasuredSets` `MeasureTheory.instSetLikeMeasuredSets` `EDist.edist` `PseudoEMetricSpace.toEDist` `MeasureTheory.instPseudoEMetricSpaceMeasuredSets`	—	`LE.le.trans` `MeasureTheory.le_measure_diff` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.subset_union_left`

---

← Back to Index