Real

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

Statistics

Metric	Count
Definitions `evalMeasureReal`	1
Theorems `exists_nonempty_inter_of_measureReal_univ_lt_sum_measureReal`, `le_measureReal_diff`, `map_measureReal_apply`, `measureReal_add_apply`, `measureReal_add_diff`, `measureReal_add_measureReal_compl`, `measureReal_add_measureReal_compl₀`, `measureReal_biUnion_finset`, `measureReal_biUnion_finset_le`, `measureReal_biUnion_finset₀`, `measureReal_compl`, `measureReal_compl₀`, `measureReal_congr`, `measureReal_diff`, `measureReal_diff'`, `measureReal_diff_add_inter`, `measureReal_diff_le_iff_le_add`, `measureReal_diff_lt_of_lt_add`, `measureReal_diff_null`, `measureReal_diff_null'`, `measureReal_empty`, `measureReal_ennreal_smul_apply`, `measureReal_eq_measureReal_iff`, `measureReal_eq_measureReal_larger_of_between_null_diff`, `measureReal_eq_measureReal_of_between_null_diff`, `measureReal_eq_measureReal_of_null_diff`, `measureReal_eq_measureReal_smaller_of_between_null_diff`, `measureReal_eq_zero_iff`, `measureReal_iUnion_fintype`, `measureReal_iUnion_fintype_le`, `measureReal_inter_add_diff`, `measureReal_inter_add_diff₀`, `measureReal_le_measureReal_union_left`, `measureReal_le_measureReal_union_right`, `measureReal_mono`, `measureReal_mono_null`, `measureReal_ne_zero_iff`, `measureReal_nnreal_smul_apply`, `measureReal_nonneg`, `measureReal_restrict_apply`, `measureReal_restrict_apply'`, `measureReal_restrict_apply_self`, `measureReal_restrict_apply_univ`, `measureReal_restrict_apply₀`, `measureReal_restrict_apply₀'`, `measureReal_symmDiff_eq`, `measureReal_symmDiff_le`, `measureReal_union`, `measureReal_union'`, `measureReal_union_add_inter`, `measureReal_union_add_inter'`, `measureReal_union_add_inter₀`, `measureReal_union_add_inter₀'`, `measureReal_union_congr_of_subset`, `measureReal_union_le`, `measureReal_union_null`, `measureReal_union_null_iff`, `measureReal_union₀`, `measureReal_union₀'`, `measureReal_univ_eq_one`, `measureReal_univ_ne_zero`, `measureReal_univ_pos`, `measureReal_zero`, `measureReal_zero_apply`, `nonempty_inter_of_measureReal_lt_add`, `nonempty_inter_of_measureReal_lt_add'`, `nonempty_of_measureReal_ne_zero`, `ofReal_measureReal`, `probReal_compl_eq_one_sub`, `probReal_compl_eq_one_sub₀`, `sum_measureReal_le_measureReal_univ`, `sum_measureReal_preimage_singleton`, `sum_measureReal_singleton`	73
Total	74

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalMeasureReal` 📖	CompOp	—

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_nonempty_inter_of_measureReal_univ_lt_sum_measureReal` 📖	mathematical	`MeasurableSet` `Real` `Real.instLT` `Measure.real` `Set.univ` `Finset.sum` `Real.instAddCommMonoid`	`Finset` `Finset.instMembership` `Set.Nonempty` `Set` `Set.instInter`	—	`exists_nonempty_inter_of_measure_univ_lt_sum_measure` `MeasurableSet.nullMeasurableSet` `ENNReal.toReal_lt_toReal` `measure_ne_top` `LT.lt.ne` `ENNReal.sum_lt_top` `measure_lt_top` `ENNReal.toReal_sum` `Finset.sum_congr`
`le_measureReal_diff` 📖	mathematical	`ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Real` `Real.instLE` `Real.instSub` `Measure.real` `Set.instSDiff`	—	`AddGroup.toOrderedSub` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `measureReal_le_measureReal_union_right` `Set.union_diff_self` `measureReal_union_le`
`map_measureReal_apply` 📖	mathematical	`Measurable` `MeasurableSet`	`Measure.real` `Measure.map` `Set.preimage`	—	`Measure.map_apply`
`measureReal_add_apply` 📖	mathematical	`ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Measure.real` `Measure.instAdd` `Real` `Real.instAdd`	—	`ENNReal.toReal_add`
`measureReal_add_diff` 📖	mathematical	`MeasurableSet` `ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Real` `Real.instAdd` `Measure.real` `Set.instSDiff` `Set.instUnion`	—	`measureReal_union'` `Set.disjoint_sdiff_right` `measure_ne_top_of_subset` `Set.diff_subset` `Set.union_diff_self`
`measureReal_add_measureReal_compl` 📖	mathematical	`MeasurableSet`	`Real` `Real.instAdd` `Measure.real` `Compl.compl` `Set` `Set.instCompl` `Set.univ`	—	`measureReal_add_measureReal_compl₀` `MeasurableSet.nullMeasurableSet`
`measureReal_add_measureReal_compl₀` 📖	mathematical	`NullMeasurableSet`	`Real` `Real.instAdd` `Measure.real` `Compl.compl` `Set` `Set.instCompl` `Set.univ`	—	`measureReal_union₀'` `aedisjoint_compl_right` `measure_ne_top` `Set.union_compl_self`
`measureReal_biUnion_finset` 📖	mathematical	`Set.PairwiseDisjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Finset` `Finset.instSetLike` `MeasurableSet`	`Measure.real` `Set.iUnion` `Finset.instMembership` `Finset.sum` `Real` `Real.instAddCommMonoid`	—	`measureReal_biUnion_finset₀` `Set.PairwiseDisjoint.aedisjoint` `MeasurableSet.nullMeasurableSet`
`measureReal_biUnion_finset_le` 📖	mathematical	—	`Real` `Real.instLE` `Measure.real` `Set.iUnion` `Finset` `Finset.instMembership` `Finset.sum` `Real.instAddCommMonoid`	—	`Finset.induction_on` `Set.iUnion_congr_Prop` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `measureReal_empty` `Set.iUnion_iUnion_eq_or_left` `Finset.sum_insert` `LE.le.trans` `measureReal_union_le` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`measureReal_biUnion_finset₀` 📖	mathematical	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `Function.onFun` `Set` `AEDisjoint` `NullMeasurableSet`	`Measure.real` `Set.iUnion` `Finset.instMembership` `Finset.sum` `Real` `Real.instAddCommMonoid`	—	`measure_biUnion_finset₀` `ENNReal.toReal_sum` `Finset.sum_congr`
`measureReal_compl` 📖	mathematical	`MeasurableSet`	`Measure.real` `Compl.compl` `Set` `Set.instCompl` `Real` `Real.instSub` `Set.univ`	—	`Set.compl_eq_univ_diff` `measureReal_diff` `Set.subset_univ` `measure_ne_top`
`measureReal_compl₀` 📖	mathematical	`NullMeasurableSet`	`Measure.real` `Compl.compl` `Set` `Set.instCompl` `Real` `Real.instSub` `Set.univ`	—	`Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `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_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `neg_eq_zero` `sub_eq_zero_of_eq` `measureReal_add_measureReal_compl₀`
`measureReal_congr` 📖	mathematical	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	`Measure.real`	—	`Measure.instOuterMeasureClass` `measure_congr`
`measureReal_diff` 📖	mathematical	`Set` `Set.instHasSubset` `MeasurableSet` `ENNReal` `DFunLike.coe` `Measure` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Measure.real` `Set.instSDiff` `Real` `Real.instSub`	—	`measureReal_diff'` `measure_ne_top_of_subset` `Set.union_eq_self_of_subset_right`
`measureReal_diff'` 📖	mathematical	`MeasurableSet` `ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Measure.real` `Set.instSDiff` `Real` `Real.instSub` `Set.instUnion`	—	`Set.union_comm` `measureReal_add_diff` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `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_add_lt` `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.Ring.add_pf_zero_add`
`measureReal_diff_add_inter` 📖	mathematical	`MeasurableSet` `ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Real` `Real.instAdd` `Measure.real` `Set.instSDiff` `Set.instInter`	—	`add_comm` `measureReal_inter_add_diff`
`measureReal_diff_le_iff_le_add` 📖	mathematical	`MeasurableSet` `Set` `Set.instHasSubset` `ENNReal` `DFunLike.coe` `Measure` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Real` `Real.instLE` `Measure.real` `Set.instSDiff` `Real.instAdd`	—	`measureReal_diff` `tsub_le_iff_left` `AddGroup.toOrderedSub` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`measureReal_diff_lt_of_lt_add` 📖	mathematical	`MeasurableSet` `Set` `Set.instHasSubset` `Real` `Real.instLT` `Measure.real` `Real.instAdd` `ENNReal` `DFunLike.coe` `Measure` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Set.instSDiff`	—	`measureReal_diff` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `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.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le`
`measureReal_diff_null` 📖	mathematical	`Measure.real` `Real` `Real.instZero` `ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Set.instSDiff`	—	`eq_top_or_lt_top` `measure_diff_eq_top` `measureReal_diff_null'` `measureReal_mono_null` `Set.inter_subset_right` `LT.lt.ne`
`measureReal_diff_null'` 📖	mathematical	`Measure.real` `Set` `Set.instInter` `Real` `Real.instZero` `ENNReal` `DFunLike.coe` `Measure` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Set.instSDiff`	—	`measure_diff_null'` `measureReal_eq_zero_iff` `measure_ne_top_of_subset` `Set.inter_subset_left`
`measureReal_empty` 📖	mathematical	—	`Measure.real` `Set` `Set.instEmptyCollection` `Real` `Real.instZero`	—	`measure_empty` `Measure.instOuterMeasureClass`
`measureReal_ennreal_smul_apply` 📖	mathematical	—	`Measure.real` `ENNReal` `Measure` `Measure.instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `Real` `Real.instMul` `ENNReal.toReal`	—	`IsScalarTower.right` `ENNReal.toReal_mul`
`measureReal_eq_measureReal_iff` 📖	mathematical	`ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Measure.real`	—	`ENNReal.toReal_eq_toReal_iff'`
`measureReal_eq_measureReal_larger_of_between_null_diff` 📖	—	`Set` `Set.instHasSubset` `Measure.real` `Set.instSDiff` `Real` `Real.instZero` `ENNReal` `DFunLike.coe` `Measure` `Measure.instFunLike` `Top.top` `instTopENNReal`	—	—	`measureReal_eq_measureReal_of_between_null_diff`
`measureReal_eq_measureReal_of_between_null_diff` 📖	—	`Set` `Set.instHasSubset` `Measure.real` `Set.instSDiff` `Real` `Real.instZero` `ENNReal` `DFunLike.coe` `Measure` `Measure.instFunLike` `Top.top` `instTopENNReal`	—	—	`measure_eq_measure_of_between_null_diff` `measureReal_eq_zero_iff`
`measureReal_eq_measureReal_of_null_diff` 📖	—	`Set` `Set.instHasSubset` `Measure.real` `Set.instSDiff` `Real` `Real.instZero` `ENNReal` `DFunLike.coe` `Measure` `Measure.instFunLike` `Top.top` `instTopENNReal`	—	—	`measure_eq_measure_of_null_diff` `measureReal_eq_zero_iff`
`measureReal_eq_measureReal_smaller_of_between_null_diff` 📖	—	`Set` `Set.instHasSubset` `Measure.real` `Set.instSDiff` `Real` `Real.instZero` `ENNReal` `DFunLike.coe` `Measure` `Measure.instFunLike` `Top.top` `instTopENNReal`	—	—	`measureReal_eq_measureReal_of_between_null_diff`
`measureReal_eq_zero_iff` 📖	mathematical	`ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Measure.real` `Real` `Real.instZero` `instZeroENNReal`	—	`Measure.real.eq_1` `ENNReal.toReal_eq_zero_iff`
`measureReal_iUnion_fintype` 📖	mathematical	`Pairwise` `Function.onFun` `Set` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `MeasurableSet`	`Measure.real` `Set.iUnion` `Finset.sum` `Real` `Real.instAddCommMonoid` `Finset.univ`	—	`Finset.sum_congr` `measure_iUnion` `Finite.to_countable` `Finite.of_fintype` `tsum_fintype` `SummationFilter.instLeAtTopUnconditional` `ENNReal.toReal_sum`
`measureReal_iUnion_fintype_le` 📖	mathematical	—	`Real` `Real.instLE` `Measure.real` `Set.iUnion` `Finset.sum` `Real.instAddCommMonoid` `Finset.univ`	—	`Set.iUnion_congr_Prop` `Set.iUnion_true` `measureReal_biUnion_finset_le`
`measureReal_inter_add_diff` 📖	mathematical	`MeasurableSet` `ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Real` `Real.instAdd` `Measure.real` `Set.instInter` `Set.instSDiff`	—	`ENNReal.toReal_add` `measure_ne_top_of_subset` `Set.inter_subset_left` `Set.diff_subset` `measure_inter_add_diff`
`measureReal_inter_add_diff₀` 📖	mathematical	`NullMeasurableSet` `ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Real` `Real.instAdd` `Measure.real` `Set.instInter` `Set.instSDiff`	—	`ENNReal.toReal_add` `measure_ne_top_of_subset` `Set.inter_subset_left` `Set.diff_subset` `measure_inter_add_diff₀`
`measureReal_le_measureReal_union_left` 📖	mathematical	`ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Real` `Real.instLE` `Measure.real` `Set.instUnion`	—	`eq_top_or_lt_top` `measureReal_mono` `Set.subset_union_left` `LT.lt.ne` `measure_union_lt_top` `Ne.lt_top`
`measureReal_le_measureReal_union_right` 📖	mathematical	`ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Real` `Real.instLE` `Measure.real` `Set.instUnion`	—	`Set.union_comm` `measureReal_le_measureReal_union_left`
`measureReal_mono` 📖	mathematical	`Set` `Set.instHasSubset` `ENNReal` `DFunLike.coe` `Measure` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Real` `Real.instLE` `Measure.real`	—	`ENNReal.toReal_mono` `measure_mono` `Measure.instOuterMeasureClass`
`measureReal_mono_null` 📖	—	`Set` `Set.instHasSubset` `Measure.real` `Real` `Real.instZero` `ENNReal` `DFunLike.coe` `Measure` `Measure.instFunLike` `Top.top` `instTopENNReal`	—	—	`measure_mono_null` `Measure.instOuterMeasureClass` `measureReal_eq_zero_iff`
`measureReal_ne_zero_iff` 📖	—	`ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	—	—	—
`measureReal_nnreal_smul_apply` 📖	mathematical	—	`Measure.real` `NNReal` `Measure` `Measure.instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `Real` `Real.instMul` `NNReal.toReal`	—	`IsScalarTower.right` `ENNReal.toReal_mul`
`measureReal_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `Measure.real`	—	`ENNReal.toReal_nonneg`
`measureReal_restrict_apply` 📖	mathematical	`MeasurableSet`	`Measure.real` `Measure.restrict` `Set` `Set.instInter`	—	`Measure.restrict_apply`
`measureReal_restrict_apply'` 📖	mathematical	`MeasurableSet`	`Measure.real` `Measure.restrict` `Set` `Set.instInter`	—	`Measure.restrict_apply'`
`measureReal_restrict_apply_self` 📖	mathematical	—	`Measure.real` `Measure.restrict`	—	`Measure.restrict_apply_self`
`measureReal_restrict_apply_univ` 📖	mathematical	—	`Measure.real` `Measure.restrict` `Set.univ`	—	`measureReal_restrict_apply` `Set.univ_inter`
`measureReal_restrict_apply₀` 📖	mathematical	`NullMeasurableSet` `Measure.restrict`	`Measure.real` `Set` `Set.instInter`	—	`Measure.restrict_apply₀`
`measureReal_restrict_apply₀'` 📖	mathematical	`NullMeasurableSet`	`DFunLike.coe` `Measure` `Set` `ENNReal` `Measure.instFunLike` `Measure.restrict` `Set.instInter`	—	`Measure.restrict_apply₀'`
`measureReal_symmDiff_eq` 📖	mathematical	`MeasurableSet` `ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Measure.real` `symmDiff` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.instSDiff` `Real` `Real.instAdd`	—	`ENNReal.toReal_add` `measure_ne_top_of_subset` `Set.diff_subset` `measure_symmDiff_eq` `MeasurableSet.nullMeasurableSet`
`measureReal_symmDiff_le` 📖	mathematical	`ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Real` `Real.instLE` `Measure.real` `symmDiff` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.instSDiff` `Real.instAdd`	—	`eq_top_or_lt_top` `measure_symmDiff_eq_top` `add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `ENNReal.toReal_nonneg` `le_trans` `measureReal_mono` `symmDiff_triangle` `measure_union_ne_top` `measure_symmDiff_ne_top` `ne_top_of_lt` `measureReal_union_le`
`measureReal_union` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `MeasurableSet` `ENNReal` `DFunLike.coe` `Measure` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Measure.real` `Set.instUnion` `Real` `Real.instAdd`	—	`measureReal_union₀` `MeasurableSet.nullMeasurableSet` `Disjoint.aedisjoint`
`measureReal_union'` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `MeasurableSet` `ENNReal` `DFunLike.coe` `Measure` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Measure.real` `Set.instUnion` `Real` `Real.instAdd`	—	`measureReal_union₀'` `MeasurableSet.nullMeasurableSet` `Disjoint.aedisjoint`
`measureReal_union_add_inter` 📖	mathematical	`MeasurableSet` `ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Real` `Real.instAdd` `Measure.real` `Set.instUnion` `Set.instInter`	—	`measureReal_union_add_inter₀` `MeasurableSet.nullMeasurableSet`
`measureReal_union_add_inter'` 📖	mathematical	`MeasurableSet` `ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Real` `Real.instAdd` `Measure.real` `Set.instUnion` `Set.instInter`	—	`measureReal_union_add_inter₀'` `MeasurableSet.nullMeasurableSet`
`measureReal_union_add_inter₀` 📖	mathematical	`NullMeasurableSet` `ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Real` `Real.instAdd` `Measure.real` `Set.instUnion` `Set.instInter`	—	`LT.lt.ne` `LE.le.trans_lt` `measure_union_le` `Measure.instOuterMeasureClass` `ENNReal.add_lt_top` `Ne.lt_top` `measureReal_inter_add_diff₀` `Set.union_inter_cancel_right` `Set.union_diff_right` `Set.inter_isAssoc` `Set.inter_isComm` `AddSemigroup.to_isAssociative` `AddCommMagma.to_isCommutative`
`measureReal_union_add_inter₀'` 📖	mathematical	`NullMeasurableSet` `ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Real` `Real.instAdd` `Measure.real` `Set.instUnion` `Set.instInter`	—	`Set.union_comm` `Set.inter_comm` `measureReal_union_add_inter₀` `add_comm`
`measureReal_union_congr_of_subset` 📖	mathematical	`Set` `Set.instHasSubset` `Real` `Real.instLE` `Measure.real` `ENNReal` `DFunLike.coe` `Measure` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Set.instUnion`	—	`measure_union_congr_of_subset` `ENNReal.toReal_le_toReal` `measure_ne_top_of_subset`
`measureReal_union_le` 📖	mathematical	—	`Real` `Real.instLE` `Measure.real` `Set` `Set.instUnion` `Real.instAdd`	—	`eq_top_or_lt_top` `add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `ENNReal.toReal_nonneg` `measure_ne_top_of_subset` `Set.subset_union_left` `LT.lt.ne` `Set.subset_union_right` `ENNReal.toReal_add` `ENNReal.toReal_mono` `measure_union_le` `Measure.instOuterMeasureClass`
`measureReal_union_null` 📖	mathematical	`Measure.real` `Real` `Real.instZero`	`Set` `Set.instUnion`	—	`le_antisymm` `LE.le.trans` `measureReal_union_le` `add_zero` `measureReal_nonneg`
`measureReal_union_null_iff` 📖	mathematical	`ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Measure.real` `Set.instUnion` `Real` `Real.instZero`	—	`measureReal_mono_null` `Set.subset_union_left` `measure_union_ne_top` `Set.subset_union_right` `measureReal_union_null`
`measureReal_union₀` 📖	mathematical	`NullMeasurableSet` `AEDisjoint` `ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Measure.real` `Set.instUnion` `Real` `Real.instAdd`	—	`measure_union₀` `ENNReal.toReal_add`
`measureReal_union₀'` 📖	mathematical	`NullMeasurableSet` `AEDisjoint` `ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Measure.real` `Set.instUnion` `Real` `Real.instAdd`	—	`Set.union_comm` `measureReal_union₀` `AEDisjoint.symm` `add_comm`
`measureReal_univ_eq_one` 📖	mathematical	—	`Measure.real` `Set.univ` `Real` `Real.instOne`	—	`probReal_univ`
`measureReal_univ_ne_zero` 📖	—	—	—	—	`LT.lt.ne'` `measureReal_univ_pos`
`measureReal_univ_pos` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `Measure.real` `Set.univ`	—	`ENNReal.toReal_pos` `Measure.instNeZeroENNRealCoeSetUniv` `measure_ne_top`
`measureReal_zero` 📖	mathematical	—	`Measure.real` `Measure` `Measure.instZero` `Pi.instZero` `Set` `Real` `Real.instZero`	—	—
`measureReal_zero_apply` 📖	mathematical	—	`Measure.real` `Measure` `Measure.instZero` `Real` `Real.instZero`	—	—
`nonempty_inter_of_measureReal_lt_add` 📖	mathematical	`MeasurableSet` `Set` `Set.instHasSubset` `Real` `Real.instLT` `Measure.real` `Real.instAdd` `ENNReal` `DFunLike.coe` `Measure` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Set.Nonempty` `Set.instInter`	—	`nonempty_inter_of_measure_lt_add` `ENNReal.toReal_lt_toReal` `ENNReal.add_ne_top` `measure_ne_top_of_subset` `ENNReal.toReal_add`
`nonempty_inter_of_measureReal_lt_add'` 📖	mathematical	`MeasurableSet` `Set` `Set.instHasSubset` `Real` `Real.instLT` `Measure.real` `Real.instAdd` `ENNReal` `DFunLike.coe` `Measure` `Measure.instFunLike` `Top.top` `instTopENNReal`	`Set.Nonempty` `Set.instInter`	—	`Set.inter_comm` `nonempty_inter_of_measureReal_lt_add` `add_comm`
`nonempty_of_measureReal_ne_zero` 📖	mathematical	—	`Set.Nonempty`	—	`Set.nonempty_iff_ne_empty` `measureReal_empty`
`ofReal_measureReal` 📖	mathematical	`ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	`ENNReal.ofReal` `Measure.real`	—	`ENNReal.ofReal_toReal`
`probReal_compl_eq_one_sub` 📖	mathematical	`MeasurableSet`	`Measure.real` `Compl.compl` `Set` `Set.instCompl` `Real` `Real.instSub` `Real.instOne`	—	`probReal_compl_eq_one_sub₀` `MeasurableSet.nullMeasurableSet`
`probReal_compl_eq_one_sub₀` 📖	mathematical	`NullMeasurableSet`	`Measure.real` `Compl.compl` `Set` `Set.instCompl` `Real` `Real.instSub` `Real.instOne`	—	`measureReal_compl₀` `IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `probReal_univ`
`sum_measureReal_le_measureReal_univ` 📖	mathematical	`MeasurableSet` `Set.PairwiseDisjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Finset` `Finset.instSetLike`	`Real` `Real.instLE` `Finset.sum` `Real.instAddCommMonoid` `Measure.real` `Set.univ`	—	`Finset.sum_congr` `ENNReal.toReal_sum` `measure_ne_top` `ENNReal.toReal_mono` `sum_measure_le_measure_univ` `MeasurableSet.nullMeasurableSet` `Set.PairwiseDisjoint.aedisjoint`
`sum_measureReal_preimage_singleton` 📖	mathematical	`MeasurableSet` `Set.preimage` `Set` `Set.instSingletonSet`	`Finset.sum` `Real` `Real.instAddCommMonoid` `Measure.real` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`Finset.sum_congr` `sum_measure_preimage_singleton` `ENNReal.toReal_sum`
`sum_measureReal_singleton` 📖	mathematical	—	`Finset.sum` `Real` `Real.instAddCommMonoid` `Measure.real` `Set` `Set.instSingletonSet` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`Finset.sum_congr` `ENNReal.toReal_sum` `ne_of_lt` `measure_singleton_lt_top` `sum_measure_singleton`

---

← Back to Index