MutuallySingular

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

Statistics

Metric	Count
Definitions `MutuallySingular`, `nullSet`, `MutuallySingular`, `«term_⟂ₘ_»`	4
Theorems `mutuallySingular_map`, `add_left`, `add_left_iff`, `add_right`, `add_right_iff`, `comm`, `congr_ac`, `disjoint`, `disjoint_ae`, `measurableSet_nullSet`, `measure_compl_nullSet`, `measure_nullSet`, `mk`, `mono`, `mono_ac`, `restrict`, `restrict_compl_nullSet`, `restrict_nullSet`, `self_iff`, `smul`, `smul_nnreal`, `sum_left`, `sum_right`, `zero_left`, `zero_right`, `absolutelyContinuous_of_add_of_mutuallySingular`, `disjoint_of_disjoint_ae`, `eq_zero_of_absolutelyContinuous_of_mutuallySingular`, `exists_null_set_measure_lt_of_disjoint`, `mutuallySingular_iff_disjoint`, `mutuallySingular_iff_disjoint_ae`, `mutuallySingular_of_disjoint`, `mutuallySingular_tfae`	33
Total	37

MeasurableEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mutuallySingular_map` 📖	mathematical	`MeasurableEmbedding` `MeasureTheory.Measure.MutuallySingular`	`MeasureTheory.Measure.map`	—	`measurableSet_image'` `MeasureTheory.Measure.MutuallySingular.measurableSet_nullSet` `map_apply` `Function.Injective.preimage_image` `injective` `MeasureTheory.Measure.MutuallySingular.measure_nullSet` `Set.preimage_compl` `MeasureTheory.Measure.MutuallySingular.measure_compl_nullSet`

MeasureTheory

Definitions

Name	Category	Theorems
`«term_⟂ₘ_»` 📖	CompOp	—

MeasureTheory.Measure

Definitions

Name	Category	Theorems
`MutuallySingular` 📖	MathDef	38 math math: `MeasureTheory.mutuallySingular_dirac`, `singularPart_eq_self`, `mutuallySingular_tfae`, `MeasureTheory.SignedMeasure.totalVariation_mutuallySingular_iff`, `ProbabilityTheory.Kernel.mutuallySingular_singularPart`, `MeasureTheory.SignedMeasure.mutuallySingular_ennreal_iff`, `singularPart_def`, `mutually_singular_measure_sub`, `MutuallySingular.comm`, `mutuallySingular_compProd_right_iff`, `MeasureTheory.SignedMeasure.singularPart_mutuallySingular`, `MutuallySingular.mk`, `MeasureTheory.SignedMeasure.mutuallySingular_iff`, `withDensity_rnDeriv_eq_zero`, `mutuallySingular_iff_disjoint`, `mutuallySingular_compProd_iff`, `HaveLebesgueDecomposition.lebesgue_decomposition`, `ProbabilityTheory.Kernel.measurableSet_mutuallySingular`, `MutuallySingular.zero_left`, `MutuallySingular.congr_ac`, `mutuallySingular_iff_disjoint_ae`, `MutuallySingular.zero_right`, `rnDeriv_def`, `MeasureTheory.withDensity_ofReal_mutuallySingular`, `MutuallySingular.add_left_iff`, `MutuallySingular.sum_right`, `MeasureTheory.SignedMeasure.jordanDecomposition_add_withDensity_mutuallySingular`, `ProbabilityTheory.Kernel.withDensity_rnDeriv_eq_zero_iff_mutuallySingular`, `mutuallySingular_compProd_left_iff`, `MutuallySingular.self_iff`, `mutuallySingular_singularPart`, `MutuallySingular.sum_left`, `rnDeriv_eq_zero`, `AbsolutelyContinuous.mutuallySingular_compProd_iff`, `haveLebesgueDecomposition_spec`, `mutuallySingular_of_disjoint`, `MutuallySingular.add_right_iff`, `MeasureTheory.JordanDecomposition.mutuallySingular`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`absolutelyContinuous_of_add_of_mutuallySingular` 📖	—	`AbsolutelyContinuous` `MeasureTheory.Measure` `instAdd` `MutuallySingular`	—	—	`MutuallySingular.measurableSet_nullSet` `MutuallySingular.measure_nullSet` `MutuallySingular.measure_compl_nullSet` `Set.inter_union_compl` `MeasureTheory.measure_union` `Disjoint.inter_left'` `Disjoint.inter_right'` `disjoint_compl_right` `MeasurableSet.inter` `MeasurableSet.compl` `MeasureTheory.measure_inter_null_of_null_right` `zero_add` `Unique.instSubsingleton` `MeasureTheory.measure_inter_null_of_null_left`
`disjoint_of_disjoint_ae` 📖	mathematical	`Disjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass`	`instPartialOrder` `instCompleteLattice`	—	`instOuterMeasureClass` `disjoint_iff_inf_le` `le_intro` `inf_apply` `ENNReal.instCanonicallyOrderedAdd` `csInf_eq_bot_of_bot_mem` `bot_eq_zero'` `MeasureTheory.measure_mono_null` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.inter_subset_left` `Disjoint.subset_compl_left` `add_zero`
`eq_zero_of_absolutelyContinuous_of_mutuallySingular` 📖	mathematical	`AbsolutelyContinuous` `MutuallySingular`	`MeasureTheory.Measure` `instZero`	—	`MutuallySingular.self_iff` `MutuallySingular.mono_ac` `AbsolutelyContinuous.rfl`
`exists_null_set_measure_lt_of_disjoint` 📖	mathematical	`Disjoint` `MeasureTheory.Measure` `instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `instCompleteLattice` `NNReal` `Preorder.toLT` `instPartialOrderNNReal` `instZeroNNReal`	`DFunLike.coe` `Set` `ENNReal` `instFunLike` `instZeroENNReal` `ENNReal.instPartialOrder` `Compl.compl` `Set.instCompl` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `ENNReal.ofNNReal`	—	`le_bot_iff` `inf_le_left` `inf_le_right` `Nat.instAtLeastTwoHAddOfNat` `exists_lt_of_csInf_lt` `MeasureTheory.measure_empty` `instOuterMeasureClass` `Set.compl_empty` `zero_add` `ENNReal.mul_pos` `Nat.cast_zero` `LT.lt.ne` `one_div` `isReduced_of_noZeroDivisors` `ENNReal.instNoZeroDivisors` `Set.inter_univ` `inf_apply` `MeasurableSet.univ` `ENNReal.eq_zero_of_le_mul_pow` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `ENNReal.instCharZero` `LE.le.trans` `MeasureTheory.measure_mono` `Set.iInter_subset_of_subset` `le_add_right` `ENNReal.instCanonicallyOrderedAdd` `le_rfl` `LT.lt.le` `Set.compl_iInter` `mul_comm` `ENNReal.tsum_mul_left` `ENNReal.tsum_geometric` `ENNReal.one_sub_inv_two` `inv_inv` `MeasureTheory.measure_iUnion_le` `instCountableNat` `Summable.tsum_le_tsum` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `SummationFilter.instNeBotUnconditional` `le_add_left` `ENNReal.summable`
`mutuallySingular_iff_disjoint` 📖	mathematical	—	`MutuallySingular` `Disjoint` `MeasureTheory.Measure` `instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `instCompleteLattice`	—	`List.TFAE.out` `instOuterMeasureClass` `mutuallySingular_tfae`
`mutuallySingular_iff_disjoint_ae` 📖	mathematical	—	`MutuallySingular` `Disjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass`	—	`List.TFAE.out` `instOuterMeasureClass` `mutuallySingular_tfae`
`mutuallySingular_of_disjoint` 📖	mathematical	`Disjoint` `MeasureTheory.Measure` `instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `instCompleteLattice`	`MutuallySingular`	—	`Nat.instAtLeastTwoHAddOfNat` `pow_succ` `mul_assoc` `mul_comm` `Nat.cast_one` `div_mul_cancel₀` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `one_mul` `one_div` `ENNReal.coe_inv` `exists_null_set_measure_lt_of_disjoint` `pow_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `NNReal.instIsOrderedRing` `MeasureTheory.measure_iUnion_null` `instOuterMeasureClass` `instCountableNat` `Set.compl_iUnion` `ENNReal.eq_zero_of_le_mul_pow` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `ENNReal.instCharZero` `ENNReal.coe_one` `LE.le.trans` `MeasureTheory.measure_mono` `Set.iInter_subset_of_subset` `Set.union_compl_self` `subset_refl` `Set.instReflSubset`
`mutuallySingular_tfae` 📖	mathematical	—	`List.TFAE` `MutuallySingular` `Disjoint` `MeasureTheory.Measure` `instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `instCompleteLattice` `Filter` `Filter.instPartialOrder` `Filter.instCompleteLatticeFilter` `MeasureTheory.ae` `instFunLike` `instOuterMeasureClass`	—	`MutuallySingular.disjoint` `mutuallySingular_of_disjoint` `instOuterMeasureClass` `MutuallySingular.disjoint_ae` `disjoint_of_disjoint_ae` `List.tfae_of_cycle`

MeasureTheory.Measure.MutuallySingular

Definitions

Name	Category	Theorems
`nullSet` 📖	CompOp	5 math math: `restrict_nullSet`, `measurableSet_nullSet`, `measure_nullSet`, `measure_compl_nullSet`, `restrict_compl_nullSet`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_left` 📖	mathematical	`MeasureTheory.Measure.MutuallySingular`	`MeasureTheory.Measure` `MeasureTheory.Measure.instAdd`	—	`add_left_iff`
`add_left_iff` 📖	mathematical	—	`MeasureTheory.Measure.MutuallySingular` `MeasureTheory.Measure` `MeasureTheory.Measure.instAdd`	—	`MeasureTheory.Measure.sum_cond` `sum_left` `Bool.countable`
`add_right` 📖	mathematical	`MeasureTheory.Measure.MutuallySingular`	`MeasureTheory.Measure` `MeasureTheory.Measure.instAdd`	—	`add_right_iff`
`add_right_iff` 📖	mathematical	—	`MeasureTheory.Measure.MutuallySingular` `MeasureTheory.Measure` `MeasureTheory.Measure.instAdd`	—	`comm` `add_left_iff`
`comm` 📖	mathematical	—	`MeasureTheory.Measure.MutuallySingular`	—	`symm`
`congr_ac` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous`	`MeasureTheory.Measure.MutuallySingular`	—	`mono_ac`
`disjoint` 📖	mathematical	`MeasureTheory.Measure.MutuallySingular`	`Disjoint` `MeasureTheory.Measure` `MeasureTheory.Measure.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `MeasureTheory.Measure.instCompleteLattice`	—	`le_bot_iff` `MeasureTheory.Measure.ext` `Set.inter_union_compl` `MeasureTheory.measure_union` `Disjoint.mono` `Set.inter_subset_right` `disjoint_compl_right` `MeasurableSet.inter` `MeasurableSet.compl` `measurableSet_nullSet` `add_eq_zero` `Unique.instSubsingleton` `MeasureTheory.measure_inter_null_of_null_right` `MeasureTheory.Measure.absolutelyContinuous_of_le` `measure_nullSet` `measure_compl_nullSet`
`disjoint_ae` 📖	mathematical	`MeasureTheory.Measure.MutuallySingular`	`Disjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	`MeasureTheory.Measure.instOuterMeasureClass` `disjoint_iff_inf_le` `MeasureTheory.mem_ae_iff` `Set.compl_union` `compl_compl` `MeasureTheory.measure_inter_null_of_null_right` `measure_nullSet` `measure_compl_nullSet` `Set.union_eq_compl_compl_inter_compl` `Set.inter_union_compl`
`measurableSet_nullSet` 📖	mathematical	`MeasureTheory.Measure.MutuallySingular`	`MeasurableSet` `nullSet`	—	—
`measure_compl_nullSet` 📖	mathematical	`MeasureTheory.Measure.MutuallySingular`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Compl.compl` `Set.instCompl` `nullSet` `instZeroENNReal`	—	—
`measure_nullSet` 📖	mathematical	`MeasureTheory.Measure.MutuallySingular`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `nullSet` `instZeroENNReal`	—	—
`mk` 📖	mathematical	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `instZeroENNReal` `Set.instHasSubset` `Set.univ` `Set.instUnion`	`MeasureTheory.Measure.MutuallySingular`	—	`MeasureTheory.measurableSet_toMeasurable` `MeasureTheory.measure_toMeasurable` `MeasureTheory.measure_mono_null` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.subset_toMeasurable`
`mono` 📖	—	`MeasureTheory.Measure.MutuallySingular` `MeasureTheory.Measure` `Preorder.toLE` `PartialOrder.toPreorder` `MeasureTheory.Measure.instPartialOrder`	—	—	`mono_ac` `LE.le.absolutelyContinuous`
`mono_ac` 📖	—	`MeasureTheory.Measure.MutuallySingular` `MeasureTheory.Measure.AbsolutelyContinuous`	—	—	—
`restrict` 📖	mathematical	`MeasureTheory.Measure.MutuallySingular`	`MeasureTheory.Measure.restrict`	—	`measurableSet_nullSet` `MeasureTheory.Measure.restrict_apply` `MeasureTheory.measure_mono_null` `MeasureTheory.Measure.instOuterMeasureClass` `Set.inter_subset_left` `measure_nullSet` `measure_compl_nullSet`
`restrict_compl_nullSet` 📖	mathematical	`MeasureTheory.Measure.MutuallySingular`	`MeasureTheory.Measure.restrict` `Compl.compl` `Set` `Set.instCompl` `nullSet` `MeasureTheory.Measure` `MeasureTheory.Measure.instZero`	—	`measure_compl_nullSet`
`restrict_nullSet` 📖	mathematical	`MeasureTheory.Measure.MutuallySingular`	`MeasureTheory.Measure.restrict` `nullSet` `MeasureTheory.Measure` `MeasureTheory.Measure.instZero`	—	`measure_nullSet`
`self_iff` 📖	mathematical	—	`MeasureTheory.Measure.MutuallySingular` `MeasureTheory.Measure` `MeasureTheory.Measure.instZero`	—	`Set.union_compl_self` `MeasureTheory.measure_union` `disjoint_compl_right` `MeasurableSet.compl` `add_zero` `MeasureTheory.Measure.measure_univ_eq_zero` `zero_left`
`smul` 📖	mathematical	`MeasureTheory.Measure.MutuallySingular`	`ENNReal` `MeasureTheory.Measure` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right`	—	`mono_ac` `IsScalarTower.right` `MeasureTheory.Measure.AbsolutelyContinuous.smul_left` `MeasureTheory.Measure.AbsolutelyContinuous.rfl`
`smul_nnreal` 📖	mathematical	`MeasureTheory.Measure.MutuallySingular`	`NNReal` `MeasureTheory.Measure` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right`	—	`smul`
`sum_left` 📖	mathematical	—	`MeasureTheory.Measure.MutuallySingular` `MeasureTheory.Measure.sum`	—	`mono` `MeasureTheory.Measure.le_sum` `le_rfl` `MeasurableSet.iInter` `MeasureTheory.Measure.sum_apply` `ENNReal.tsum_eq_zero` `MeasureTheory.measure_mono_null` `MeasureTheory.Measure.instOuterMeasureClass` `Set.iInter_subset` `Set.compl_iInter` `MeasureTheory.measure_iUnion_null_iff`
`sum_right` 📖	mathematical	—	`MeasureTheory.Measure.MutuallySingular` `MeasureTheory.Measure.sum`	—	`comm` `sum_left`
`zero_left` 📖	mathematical	—	`MeasureTheory.Measure.MutuallySingular` `MeasureTheory.Measure` `MeasureTheory.Measure.instZero`	—	`symm` `zero_right`
`zero_right` 📖	mathematical	—	`MeasureTheory.Measure.MutuallySingular` `MeasureTheory.Measure` `MeasureTheory.Measure.instZero`	—	`MeasurableSet.empty` `MeasureTheory.measure_empty` `MeasureTheory.Measure.instOuterMeasureClass`

MeasureTheory.VectorMeasure

Definitions

Name	Category	Theorems
`MutuallySingular` 📖	MathDef	8 math math: `MutuallySingular.neg_right_iff`, `MutuallySingular.mk`, `MutuallySingular.neg_left_iff`, `MeasureTheory.SignedMeasure.mutuallySingular_ennreal_iff`, `MeasureTheory.SignedMeasure.mutuallySingular_singularPart`, `MutuallySingular.zero_left`, `MutuallySingular.zero_right`, `MeasureTheory.SignedMeasure.mutuallySingular_iff`

---

← Back to Index