Documentation Verification Report

SeparableMeasure

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

Statistics

Metric	Count
Definitions `IsSeparable`, `MeasureDense`	2
Theorems `exists_countable_measureDense`, `SecondCountableTopology`, `approx`, `completion`, `fin_meas`, `fin_meas_approx`, `indicatorConstLp_subset_closure`, `measurable`, `nonempty`, `nonempty'`, `of_generateFrom_isSetAlgebra_finite`, `of_generateFrom_isSetAlgebra_sigmaFinite`, `exists_countable_measureDense`, `instIsSeparableNullMeasurableSpaceCompletion`, `instIsSeparableOfCountablyGeneratedOfSFinite`, `isSeparable_of_sigmaFinite`, `measureDense_measurableSet`	17
Total	19

MeasureTheory

Definitions

Name	Category	Theorems
`IsSeparable` 📖	CompData	3 math math: `instIsSeparableNullMeasurableSpaceCompletion`, `instIsSeparableOfCountablyGeneratedOfSFinite`, `isSeparable_of_sigmaFinite`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_countable_measureDense` 📖	mathematical	—	`Set.Countable` `Set` `Measure.MeasureDense`	—	`IsSeparable.exists_countable_measureDense`
`instIsSeparableNullMeasurableSpaceCompletion` 📖	mathematical	—	`IsSeparable` `NullMeasurableSpace` `NullMeasurableSpace.instMeasurableSpace` `Measure.completion`	—	`exists_countable_measureDense` `Measure.MeasureDense.completion`
`instIsSeparableOfCountablyGeneratedOfSFinite` 📖	mathematical	—	`IsSeparable`	—	`isSeparable_of_sigmaFinite` `instSigmaFiniteRestrictSigmaFiniteSet` `exists_countable_measureDense` `Set.Countable.image` `MeasurableSet.inter` `Measure.MeasureDense.measurable` `measurableSet_sigmaFiniteSet` `restrict_compl_sigmaFiniteSet_eq_zero_or_top` `ne_top_of_le_ne_top` `Measure.restrict_le_self` `Measure.MeasureDense.approx` `Set.diff_eq_compl_inter` `Set.inter_symmDiff_distrib_left` `ENNReal.bot_eq_zero` `eq_bot_iff` `measure_mono` `Measure.instOuterMeasureClass` `Set.symmDiff_subset_union` `measure_union_le` `Set.inter_comm` `Measure.restrict_apply` `Set.inter_assoc` `Set.inter_compl_self` `Set.empty_inter` `measure_empty` `zero_add` `measure_inter_add_diff` `add_zero` `Set.inter_symmDiff_distrib_right` `Set.inter_self` `Measure.restrict_apply'` `eq_top_iff`
`isSeparable_of_sigmaFinite` 📖	mathematical	—	`IsSeparable`	—	`MeasurableSpace.countable_countableGeneratingSet` `MeasurableSpace.generateFrom_countableGeneratingSet` `Set.countable_union` `Set.countable_iff_exists_subset_range` `countable_generateSetAlgebra` `Measure.MeasureDense.of_generateFrom_isSetAlgebra_sigmaFinite` `isSetAlgebra_generateSetAlgebra` `self_subset_generateSetAlgebra` `Measure.FiniteSpanningSetsIn.finite` `Measure.FiniteSpanningSetsIn.spanning` `le_antisymm` `MeasurableSpace.generateFrom_mono` `le_trans` `generateSetAlgebra_mono` `Set.subset_union_left` `MeasurableSpace.generateFrom_le` `MeasurableSpace.measurableSet_generateFrom` `Measure.FiniteSpanningSetsIn.set_mem` `MeasurableSet.empty` `MeasurableSet.compl` `MeasurableSet.union`
`measureDense_measurableSet` 📖	mathematical	—	`Measure.MeasureDense` `setOf` `Set` `MeasurableSet`	—	`symmDiff_self` `measure_empty` `Measure.instOuterMeasureClass`

MeasureTheory.IsSeparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_countable_measureDense` 📖	mathematical	—	`Set.Countable` `Set` `MeasureTheory.Measure.MeasureDense`	—	—

MeasureTheory.Lp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`SecondCountableTopology` 📖	mathematical	—	`SecondCountableTopology` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `instNormedAddCommGroup`	—	`UniformSpace.secondCountable_of_separable` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `EMetric.instIsCountablyGeneratedUniformity` `MeasureTheory.exists_countable_measureDense` `MeasureTheory.Measure.MeasureDense.fin_meas` `Set.Countable.mono` `ne_of_gt` `lt_of_lt_of_le` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `NeZero.charZero_one` `ENNReal.instCharZero` `Fact.elim` `TopologicalSpace.exists_countable_dense` `MeasureTheory.Measure.MeasureDense.measurable` `Subtype.mem` `Set.Countable.to_subtype` `Set.countable_range` `instCountableSigma` `instCountableNat` `instCountableProd` `instCountableForallOfFinite` `Finite.of_fintype` `induction` `LT.lt.ne` `SeminormedAddCommGroup.mem_closure_iff` `Real.rpow_nonneg` `ENNReal.toReal_nonneg` `Nat.instAtLeastTwoHAddOfNat` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.neg_congr` `Nat.cast_one` `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.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.mul_neg` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Meta.NormNum.isNat_lt_true` `Real.instIsOrderedRing` `RCLike.charZero_rclike` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.without_one_mul` `CancelDenoms.sub_subst` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `CancelDenoms.mul_subst` `CancelDenoms.add_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNat_mul` `ne_of_lt` `MeasureTheory.Measure.MeasureDense.indicatorConstLp_subset_closure` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `CancelDenoms.div_subst` `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` `Finset.sum_const` `Finset.univ_unique` `Finset.card_singleton` `one_smul` `simpleFunc.coe_indicatorConst` `sub_add_sub_cancel` `add_halves` `ZeroLEOneClass.neZero.two` `Real.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `lt_of_le_of_lt` `norm_add_le_of_le` `MeasureTheory.indicatorConstLp_sub` `MeasureTheory.norm_indicatorConstLp` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `le_of_lt` `mul_one` `div_mul_eq_div_mul_one_div` `mul_assoc` `one_div_mul_eq_div` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `div_le_one` `le_of_not_gt` `Mathlib.Tactic.Linarith.add_neg` `LT.lt.le` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `Fin.sum_univ_add` `Finset.sum_congr` `MeasureTheory.indicatorConstLp.congr_simp` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.const_add_termg` `norm_add_le` `Mathlib.Tactic.Ring.add_pf_add_gt` `isClosed_closure`

MeasureTheory.Measure

Definitions

Name	Category	Theorems
`MeasureDense` 📖	CompData	5 math math: `MeasureDense.of_generateFrom_isSetAlgebra_finite`, `MeasureDense.of_generateFrom_isSetAlgebra_sigmaFinite`, `MeasureTheory.exists_countable_measureDense`, `MeasureTheory.measureDense_measurableSet`, `MeasureTheory.IsSeparable.exists_countable_measureDense`

MeasureTheory.Measure.MeasureDense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`approx` 📖	mathematical	`MeasureTheory.Measure.MeasureDense` `MeasurableSet` `Real` `Real.instLT` `Real.instZero`	`Set` `Set.instMembership` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `symmDiff` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.instSDiff` `ENNReal.ofReal`	—	—
`completion` 📖	mathematical	`MeasureTheory.Measure.MeasureDense`	`MeasureTheory.NullMeasurableSpace` `MeasureTheory.NullMeasurableSpace.instMeasurableSpace` `MeasureTheory.Measure.completion`	—	`MeasurableSet.nullMeasurableSet` `measurable` `approx` `MeasureTheory.measurableSet_toMeasurable` `MeasureTheory.measure_toMeasurable` `MeasureTheory.Measure.completion_apply` `MeasureTheory.measure_congr` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_eq_set_symmDiff` `Filter.EventuallyEq.symm` `MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq` `Filter.EventuallyEq.rfl`
`fin_meas` 📖	mathematical	`MeasureTheory.Measure.MeasureDense`	`setOf` `Set` `Set.instMembership` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Top.top` `instTopENNReal`	—	`measurable` `fin_meas_approx`
`fin_meas_approx` 📖	mathematical	`MeasureTheory.Measure.MeasureDense` `MeasurableSet` `Real` `Real.instLT` `Real.instZero`	`Set` `Set.instMembership` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `symmDiff` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.instSDiff` `ENNReal.ofReal`	—	`approx` `MeasureTheory.measure_ne_top_iff_of_symmDiff` `ne_top_of_lt`
`indicatorConstLp_subset_closure` 📖	mathematical	`MeasureTheory.Measure.MeasureDense`	`Set` `MeasureTheory.AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `MeasureTheory.AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `MeasureTheory.Lp` `Set.instHasSubset` `setOf` `MeasurableSet` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Top.top` `instTopENNReal` `MeasureTheory.indicatorConstLp` `closure` `MeasureTheory.Lp.instNormedAddCommGroup` `Set.instMembership` `measurable`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `measurable` `eq_or_ne` `Set.Subset.trans` `nonempty'` `Set.indicator_zero` `MeasureTheory.MemLp.toLp.congr_simp` `subset_closure` `lt_of_lt_of_le` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `NeZero.charZero_one` `ENNReal.instCharZero` `Fact.elim` `Metric.mem_closure_iff` `Real.rpow_pos_of_pos` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `norm_pos_iff` `fin_meas_approx` `MeasurableSet.symmDiff` `MeasureTheory.measure_symmDiff_ne_top` `MeasureTheory.dist_indicatorConstLp_eq_norm` `MeasureTheory.norm_indicatorConstLp` `LT.lt.ne` `ENNReal.toReal_pos` `MeasureTheory.measureReal_def` `mul_lt_mul_of_pos_left` `Real.rpow_lt_rpow` `ENNReal.toReal_nonneg` `ENNReal.toReal_strict_mono` `ENNReal.ofReal_ne_top` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `ENNReal.toReal_ofReal` `Real.rpow_nonneg` `div_nonneg` `LT.lt.le` `norm_nonneg` `one_div` `Real.rpow_rpow_inv` `mul_div_cancel₀` `norm_ne_zero_iff`
`measurable` 📖	mathematical	`MeasureTheory.Measure.MeasureDense` `Set` `Set.instMembership`	`MeasurableSet`	—	—
`nonempty` 📖	mathematical	`MeasureTheory.Measure.MeasureDense`	`Set.Nonempty` `Set`	—	`approx` `MeasurableSet.empty` `MeasureTheory.measure_empty` `MeasureTheory.Measure.instOuterMeasureClass` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`nonempty'` 📖	mathematical	`MeasureTheory.Measure.MeasureDense`	`Set.Nonempty` `Set` `setOf` `Set.instMembership` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Top.top` `instTopENNReal`	—	`approx` `MeasurableSet.empty` `MeasureTheory.measure_empty` `MeasureTheory.Measure.instOuterMeasureClass` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Set.bot_eq_empty` `bot_symmDiff` `ne_top_of_lt`
`of_generateFrom_isSetAlgebra_finite` 📖	mathematical	`MeasureTheory.IsSetAlgebra` `MeasurableSpace.generateFrom`	`MeasureTheory.Measure.MeasureDense`	—	`MeasurableSpace.measurableSet_generateFrom` `MeasurableSpace.generateFrom_induction` `symmDiff_self` `MeasureTheory.measureReal_empty` `MeasurableSet.empty` `MeasureTheory.IsSetAlgebra.empty_mem` `MeasurableSet.compl` `MeasureTheory.IsSetAlgebra.compl_mem` `compl_symmDiff_compl` `MeasurableSet.iUnion` `instCountableNat` `MeasureTheory.tendsto_measure_iUnion_accumulate` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `PseudoEMetricSpace.pseudoMetrizableSpace` `Nat.instAtLeastTwoHAddOfNat` `Metric.tendsto_atTop` `ENNReal.tendsto_toReal_iff` `MeasureTheory.measure_ne_top` `lt_of_not_ge` `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` `Nat.cast_one` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `CancelDenoms.sub_subst` `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` `MeasureTheory.IsSetAlgebra.biUnion_mem` `ENNReal.toReal_mono` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `symmDiff_triangle` `symmDiff_of_ge` `Set.iUnion_subset` `Set.subset_iUnion` `ENNReal.toReal_add` `ENNReal.add_ne_top` `MeasureTheory.measure_union_le` `add_halves` `ZeroLEOneClass.neZero.two` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `add_lt_add` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `MeasureTheory.measure_diff` `MeasurableSet.biUnion` `Set.countable_coe_iff` `SetCoe.countable` `MeasurableSet.nullMeasurableSet` `ENNReal.toReal_sub_of_le` `lt_of_le_of_lt` `Real.sub_le_dist` `Set.iUnion_congr_Prop` `le_refl` `dist_comm` `biSup_symmDiff_biSup_le` `Finset.sum_congr` `ENNReal.toReal_sum` `ne_of_lt` `ENNReal.sum_lt_top` `MeasureTheory.measure_lt_top` `MeasureTheory.measure_biUnion_finset_le` `Finset.sum_lt_sum` `Real.instIsOrderedCancelAddMonoid` `le_of_lt` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instNoMaxOrder` `Nat.instCanonicallyOrderedAdd` `Finset.sum_const` `Finset.card_range` `nsmul_eq_mul` `Nat.cast_add` `div_mul_eq_div_mul_one_div` `mul_assoc` `mul_comm` `mul_le_of_le_one_right` `IsOrderedRing.toPosMulMono` `le_of_not_gt` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.mul_neg` `le_of_eq` `mul_one_div_cancel` `Nat.cast_add_one_ne_zero` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.mul_one` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.natCast_nonneg` `ENNReal.lt_ofReal_iff_toReal_lt`
`of_generateFrom_isSetAlgebra_sigmaFinite` 📖	mathematical	`MeasureTheory.IsSetAlgebra` `MeasurableSpace.generateFrom`	`MeasureTheory.Measure.MeasureDense`	—	`MeasurableSpace.measurableSet_generateFrom` `Set.iUnion_congr_Prop` `MeasureTheory.IsSetAlgebra.biUnion_mem` `MeasureTheory.Measure.FiniteSpanningSetsIn.set_mem` `Set.coe_toFinset` `MeasureTheory.measure_biUnion_lt_top` `Finset.finite_toSet` `MeasureTheory.Measure.FiniteSpanningSetsIn.finite` `Set.iUnion_accumulate` `MeasureTheory.Measure.FiniteSpanningSetsIn.spanning` `Set.inter_subset_inter_left` `Set.biUnion_subset_biUnion_left` `MeasureTheory.tendsto_measure_iUnion_atTop` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat` `PseudoEMetricSpace.pseudoMetrizableSpace` `Nat.instAtLeastTwoHAddOfNat` `Metric.tendsto_atTop` `ENNReal.tendsto_toReal_iff` `ne_top_of_le_ne_top` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.inter_subset_right` `Set.iUnion_subset` `lt_of_not_ge` `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` `Nat.cast_one` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `CancelDenoms.sub_subst` `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` `approx` `of_generateFrom_isSetAlgebra_finite` `MeasureTheory.Restrict.isFiniteMeasure` `ne_of_lt` `lt_of_le_of_lt` `MeasureTheory.Measure.restrict_apply_le` `Ne.lt_top` `MeasureTheory.IsSetAlgebra.inter_mem` `symmDiff_of_le` `Set.inter_subset_left` `symmDiff_comm` `Set.inter_symmDiff_distrib_right` `MeasureTheory.measure_symmDiff_le` `ENNReal.add_lt_add` `MeasureTheory.measure_diff` `MeasurableSet.nullMeasurableSet` `MeasurableSet.inter` `ENNReal.lt_ofReal_iff_toReal_lt` `ENNReal.sub_ne_top` `ENNReal.toReal_sub_of_le` `Real.sub_le_dist` `Set.univ_inter` `Set.inter_comm` `dist_comm` `Set.iUnion_inter` `le_refl` `MeasureTheory.Measure.restrict_apply'` `ENNReal.ofReal_add` `le_of_not_gt` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.mul_neg` `add_halves` `ZeroLEOneClass.neZero.two` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`

---

← Back to Index