AEDisjoint

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

Statistics

Metric	Count
Definitions AEDisjoint	1
Theorems aedisjoint, comm, diff_ae_eq_left, diff_ae_eq_right, eq, exists_disjoint_diff, iUnion_left_iff, iUnion_right_iff, measure_diff_left, measure_diff_right, mono, mono_ae, of_null_left, of_null_right, symmetric, union_left, union_left_iff, union_right, union_right_iff, aedisjoint_compl_left, aedisjoint_compl_right, exists_null_pairwise_disjoint_diff, aedisjoint, aedisjoint	24
Total	25

Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aedisjoint 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	MeasureTheory.AEDisjoint	—	MeasureTheory.AEDisjoint.eq_1 Set.disjoint_iff_inter_eq_empty MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass

MeasureTheory

Definitions

Name	Category	Theorems
AEDisjoint 📖	MathDef	17 math math: AEDisjoint.union_right_iff, aedisjoint_compl_right, AEDisjoint.of_null_left, IsFundamentalDomain.pairwise_aedisjoint_of_ac, aedisjoint_compl_left, Set.PairwiseDisjoint.aedisjoint, IsAddFundamentalDomain.pairwise_aedisjoint_of_ac, AEDisjoint.iUnion_right_iff, AEDisjoint.iUnion_left_iff, Pairwise.aedisjoint, Disjoint.aedisjoint, IsFundamentalDomain.aedisjoint, AEDisjoint.comm, AEDisjoint.of_null_right, AEDisjoint.union_left_iff, AEDisjoint.symmetric, IsAddFundamentalDomain.aedisjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aedisjoint_compl_left 📖	mathematical	—	AEDisjoint Compl.compl Set Set.instCompl	—	Disjoint.aedisjoint disjoint_compl_left
aedisjoint_compl_right 📖	mathematical	—	AEDisjoint Compl.compl Set Set.instCompl	—	Disjoint.aedisjoint disjoint_compl_right
exists_null_pairwise_disjoint_diff 📖	mathematical	Pairwise Function.onFun Set AEDisjoint	MeasurableSet DFunLike.coe Measure ENNReal Measure.instFunLike instZeroENNReal Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.instSDiff	—	measurableSet_toMeasurable Set.inter_iUnion measure_toMeasurable measure_biUnion_null_iff Measure.instOuterMeasureClass Set.to_countable SetCoe.countable subset_toMeasurable

MeasureTheory.AEDisjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm 📖	mathematical	—	MeasureTheory.AEDisjoint	—	symm
diff_ae_eq_left 📖	mathematical	MeasureTheory.AEDisjoint	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set Set.instSDiff	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.diff_null_ae_eq_self Set.diff_self_inter
diff_ae_eq_right 📖	mathematical	MeasureTheory.AEDisjoint	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Set Set.instSDiff	—	diff_ae_eq_left symm
eq 📖	mathematical	MeasureTheory.AEDisjoint	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike Set.instInter instZeroENNReal	—	—
exists_disjoint_diff 📖	mathematical	MeasureTheory.AEDisjoint	MeasurableSet DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike instZeroENNReal Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.instSDiff	—	MeasureTheory.measurableSet_toMeasurable MeasureTheory.measure_toMeasurable Disjoint.mono_left MeasureTheory.subset_toMeasurable disjoint_sdiff_self_left
iUnion_left_iff 📖	mathematical	—	MeasureTheory.AEDisjoint Set.iUnion	—	Set.iUnion_inter MeasureTheory.Measure.instOuterMeasureClass
iUnion_right_iff 📖	mathematical	—	MeasureTheory.AEDisjoint Set.iUnion	—	Set.inter_iUnion MeasureTheory.Measure.instOuterMeasureClass
measure_diff_left 📖	mathematical	MeasureTheory.AEDisjoint	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike Set.instSDiff	—	MeasureTheory.measure_congr MeasureTheory.Measure.instOuterMeasureClass diff_ae_eq_left
measure_diff_right 📖	mathematical	MeasureTheory.AEDisjoint	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike Set.instSDiff	—	MeasureTheory.measure_congr MeasureTheory.Measure.instOuterMeasureClass diff_ae_eq_right
mono 📖	—	MeasureTheory.AEDisjoint Set Set.instHasSubset	—	—	mono_ae HasSubset.Subset.eventuallyLE MeasureTheory.Measure.instOuterMeasureClass
mono_ae 📖	—	MeasureTheory.AEDisjoint Filter.EventuallyLE Prop.le MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.measure_mono_null_ae Filter.EventuallyLE.inter
of_null_left 📖	mathematical	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike instZeroENNReal	MeasureTheory.AEDisjoint	—	symm of_null_right
of_null_right 📖	mathematical	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike instZeroENNReal	MeasureTheory.AEDisjoint	—	MeasureTheory.measure_mono_null MeasureTheory.Measure.instOuterMeasureClass Set.inter_subset_right
symmetric 📖	mathematical	—	Symmetric Set MeasureTheory.AEDisjoint	—	symm
union_left 📖	mathematical	MeasureTheory.AEDisjoint	Set Set.instUnion	—	union_left_iff
union_left_iff 📖	mathematical	—	MeasureTheory.AEDisjoint Set Set.instUnion	—	Set.union_eq_iUnion Bool.countable
union_right 📖	mathematical	MeasureTheory.AEDisjoint	Set Set.instUnion	—	union_right_iff
union_right_iff 📖	mathematical	—	MeasureTheory.AEDisjoint Set Set.instUnion	—	Set.union_eq_iUnion Bool.countable

Pairwise

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aedisjoint 📖	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	MeasureTheory.AEDisjoint	—	mono Disjoint.aedisjoint

Set.PairwiseDisjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aedisjoint 📖	mathematical	Set.PairwiseDisjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Set.Pairwise Function.onFun MeasureTheory.AEDisjoint	—	Set.Pairwise.mono' Disjoint.aedisjoint

---

← Back to Index