SetSemiring

📁 Source: Mathlib/MeasureTheory/SetSemiring.lean

Statistics

Metric	Count
Definitions IsSetRing, IsSetSemiring, disjointOfDiff, disjointOfDiffUnion, disjointOfUnion, SetSemiring	6
Theorems accumulate_mem, biInter_mem, biUnion_mem, diff_mem, disjointed_mem, empty_mem, finsetSup_mem, iInter_le_mem, iUnion_le_mem, inter_mem, isSetSemiring, partialSups_mem, union_mem, Ioc, diff_eq_sUnion', diff_mem_supClosure, diff_sUnion_eq_sUnion_disjointOfDiffUnion, disjointOfDiffUnion_subset, disjointOfUnion_props, disjointOfUnion_subset, disjointOfUnion_subset_of_mem, disjoint_disjointOfDiffUnion, disjoint_sUnion_disjointOfDiff, disjoint_sUnion_disjointOfDiffUnion, empty_mem, empty_notMem_disjointOfDiff, empty_notMem_disjointOfDiffUnion, empty_notMem_disjointOfUnion, exists_disjoint_finset_diff_eq, exists_finpartition_diff, inter_mem, isPiSystem, isSetRing_supClosure, mem_supClosure_iff, notMem_disjointOfDiff, pairwiseDisjoint_biUnion_disjointOfUnion, pairwiseDisjoint_disjointOfDiff, pairwiseDisjoint_disjointOfDiffUnion, pairwiseDisjoint_disjointOfUnion, pairwiseDisjoint_disjointOfUnion_of_mem, pairwiseDisjoint_insert_disjointOfDiff, pairwiseDisjoint_union_disjointOfDiffUnion, sUnion_disjointOfDiff, sUnion_disjointOfDiffUnion_subset, sUnion_disjointOfUnion, sUnion_insert_disjointOfDiff, sUnion_union_disjointOfDiffUnion_of_subset, sUnion_union_sUnion_disjointOfDiffUnion_of_subset, subset_disjointOfDiff, subset_of_diffUnion_disjointOfDiffUnion, subset_of_mem_disjointOfDiffUnion, subset_of_mem_disjointOfUnion	52
Total	58

MeasureTheory

Definitions

Name	Category	Theorems
IsSetRing 📖	CompData	3 math math: IsSetSemiring.isSetRing_supClosure, isSetRing_measurableCylinders, IsSetAlgebra.isSetRing
IsSetSemiring 📖	CompData	3 math math: isSetSemiring_measurableCylinders, IsSetRing.isSetSemiring, IsSetSemiring.Ioc

MeasureTheory.IsSetRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
accumulate_mem 📖	mathematical	MeasureTheory.IsSetRing Set Set.instMembership	Set.accumulate	—	Set.accumulate_zero_nat Set.accumulate_succ union_mem
biInter_mem 📖	mathematical	MeasureTheory.IsSetRing Finset.Nonempty Set Set.instMembership	Set.iInter Finset Finset.instMembership	—	Finset.Nonempty.cons_induction Set.iInter_congr_Prop Set.iInter_iInter_eq_left Finset.coe_cons Set.biInter_insert inter_mem Finset.cons_eq_insert
biUnion_mem 📖	mathematical	MeasureTheory.IsSetRing Set Set.instMembership	Set.iUnion Finset Finset.instMembership	—	Finset.induction Set.iUnion_congr_Prop Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty empty_mem Finset.coe_insert Set.biUnion_insert union_mem Finset.mem_insert_self Finset.mem_insert_of_mem
diff_mem 📖	mathematical	MeasureTheory.IsSetRing Set Set.instMembership	Set.instSDiff	—	—
disjointed_mem 📖	mathematical	MeasureTheory.IsSetRing Set Set.instMembership	disjointed BooleanAlgebra.toGeneralizedBooleanAlgebra Set.instBooleanAlgebra	—	disjointedRec diff_mem
empty_mem 📖	mathematical	MeasureTheory.IsSetRing	Set Set.instMembership Set.instEmptyCollection	—	—
finsetSup_mem 📖	mathematical	MeasureTheory.IsSetRing Set Set.instMembership	Finset.sup Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	Finset.sup_set_eq_biUnion biUnion_mem
iInter_le_mem 📖	mathematical	MeasureTheory.IsSetRing Set Set.instMembership	Set.iInter	—	Set.iInter_congr_Prop Nat.instCanonicallyOrderedAdd Set.iInter_iInter_eq_left Set.biInter_le_succ inter_mem
iUnion_le_mem 📖	mathematical	MeasureTheory.IsSetRing Set Set.instMembership	Set.iUnion	—	Set.iUnion_congr_Prop Nat.instCanonicallyOrderedAdd Set.iUnion_iUnion_eq_left Set.biUnion_le_succ union_mem
inter_mem 📖	mathematical	MeasureTheory.IsSetRing Set Set.instMembership	Set.instInter	—	Set.diff_diff_right_self diff_mem
isSetSemiring 📖	mathematical	MeasureTheory.IsSetRing	MeasureTheory.IsSetSemiring	—	empty_mem inter_mem Finset.coe_singleton diff_mem Set.sUnion_singleton
partialSups_mem 📖	mathematical	MeasureTheory.IsSetRing Set Set.instMembership	DFunLike.coe OrderHom PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra OrderHom.instFunLike partialSups	—	Finset.sup'_eq_sup Finset.nonempty_Iic finsetSup_mem
union_mem 📖	mathematical	MeasureTheory.IsSetRing Set Set.instMembership	Set.instUnion	—	—

MeasureTheory.IsSetSemiring

Definitions

Name	Category	Theorems
disjointOfDiff 📖	CompOp	9 math math: pairwiseDisjoint_insert_disjointOfDiff, empty_notMem_disjointOfDiff, sUnion_disjointOfDiff, notMem_disjointOfDiff, sUnion_insert_disjointOfDiff, pairwiseDisjoint_disjointOfDiff, subset_disjointOfDiff, MeasureTheory.eq_add_disjointOfDiff_of_subset, disjoint_sUnion_disjointOfDiff
disjointOfDiffUnion 📖	CompOp	11 math math: diff_sUnion_eq_sUnion_disjointOfDiffUnion, pairwiseDisjoint_union_disjointOfDiffUnion, disjoint_sUnion_disjointOfDiffUnion, sUnion_union_disjointOfDiffUnion_of_subset, sUnion_disjointOfDiffUnion_subset, disjointOfDiffUnion_subset, MeasureTheory.addContent_eq_add_disjointOfDiffUnion_of_subset, empty_notMem_disjointOfDiffUnion, disjoint_disjointOfDiffUnion, sUnion_union_sUnion_disjointOfDiffUnion_of_subset, pairwiseDisjoint_disjointOfDiffUnion
disjointOfUnion 📖	CompOp	7 math math: empty_notMem_disjointOfUnion, pairwiseDisjoint_disjointOfUnion_of_mem, pairwiseDisjoint_biUnion_disjointOfUnion, disjointOfUnion_subset, sUnion_disjointOfUnion, pairwiseDisjoint_disjointOfUnion, disjointOfUnion_subset_of_mem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Ioc 📖	mathematical	—	MeasureTheory.IsSetSemiring setOf Set Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.Ioc	—	le_rfl Set.Ioc_eq_empty Set.Ioc_inter_Ioc le_or_gt Set.ext Finset.coe_singleton Set.sUnion_singleton Finset.coe_insert Set.sUnion_insert
diff_eq_sUnion' 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership	Set.instHasSubset SetLike.coe Finset Finset.instSetLike Set.PairwiseDisjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.instSDiff Set.sUnion	—	—
diff_mem_supClosure 📖	mathematical	MeasureTheory.IsSetSemiring 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 Set.instSDiff	—	mem_supClosure_iff exists_finpartition_diff
diff_sUnion_eq_sUnion_disjointOfDiffUnion 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership Set.instHasSubset SetLike.coe Finset Finset.instSetLike	Set.instSDiff Set.sUnion disjointOfDiffUnion	—	exists_disjoint_finset_diff_eq Finset.coe_sdiff Finset.coe_singleton Set.sUnion_diff_singleton_empty
disjointOfDiffUnion_subset 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership Set.instHasSubset SetLike.coe Finset Finset.instSetLike	disjointOfDiffUnion	—	exists_disjoint_finset_diff_eq Finset.coe_sdiff Finset.coe_singleton HasSubset.Subset.trans Set.instIsTransSubset Set.subset_insert
disjointOfUnion_props 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike	Set.PairwiseDisjoint Finset.partialOrder Finset.instOrderBot ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.iUnion Finset.instMembership Set.sUnion Set.instEmptyCollection	—	Finset.cons_induction Finset.coe_empty instIsEmptyFalse Set.iUnion_congr_Prop Set.iUnion_of_empty Set.iUnion_empty Set.sUnion_empty Set.insert_subset_iff Finset.coe_insert Finset.cons_eq_insert Set.sUnion_insert Set.iUnion₂_congr Set.Pairwise.insert Function.onFun.eq_1 disjoint_of_sSup_disjoint_of_le_of_le subset_of_diffUnion_disjointOfDiffUnion Set.sUnion_subset_iff HasSubset.Subset.trans Set.instIsTransSubset Set.subset_sUnion_of_mem Set.disjoint_sdiff_left empty_notMem_disjointOfDiffUnion Finset.disjoint_iff_inter_eq_empty Set.disjoint_iff_inter_eq_empty Disjoint.symm disjointOfDiffUnion_subset Set.iUnion_iUnion_eq_or_left Set.pairwiseDisjoint_union pairwiseDisjoint_disjointOfDiffUnion Set.disjoint_of_subset subset_trans subset_of_mem_disjointOfDiffUnion Set.sUnion_union diff_sUnion_eq_sUnion_disjointOfDiffUnion Set.diff_union_self
disjointOfUnion_subset 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike Finset.instMembership	disjointOfUnion	—	disjointOfUnion_props
disjointOfUnion_subset_of_mem 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike Finset.instMembership	Set.sUnion disjointOfUnion	—	disjointOfUnion_props
disjoint_disjointOfDiffUnion 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership Set.instHasSubset SetLike.coe Finset Finset.instSetLike	Disjoint Finset.partialOrder Finset.instOrderBot disjointOfDiffUnion	—	Finset.not_disjoint_iff disjoint_sUnion_disjointOfDiffUnion Set.subset_sUnion_of_mem empty_notMem_disjointOfDiffUnion
disjoint_sUnion_disjointOfDiff 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership	Disjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.sUnion SetLike.coe Finset Finset.instSetLike disjointOfDiff	—	sUnion_disjointOfDiff Set.disjoint_sdiff_right
disjoint_sUnion_disjointOfDiffUnion 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership Set.instHasSubset SetLike.coe Finset Finset.instSetLike	Disjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.sUnion disjointOfDiffUnion	—	diff_sUnion_eq_sUnion_disjointOfDiffUnion Set.disjoint_sdiff_right
empty_mem 📖	mathematical	MeasureTheory.IsSetSemiring	Set Set.instMembership Set.instEmptyCollection	—	—
empty_notMem_disjointOfDiff 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership	Finset Finset.instMembership disjointOfDiff Set.instEmptyCollection	—	diff_eq_sUnion'
empty_notMem_disjointOfDiffUnion 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership Set.instHasSubset SetLike.coe Finset Finset.instSetLike	Finset.instMembership disjointOfDiffUnion Set.instEmptyCollection	—	exists_disjoint_finset_diff_eq
empty_notMem_disjointOfUnion 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike Finset.instMembership	disjointOfUnion Set.instEmptyCollection	—	disjointOfUnion_props
exists_disjoint_finset_diff_eq 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership Set.instHasSubset SetLike.coe Finset Finset.instSetLike	Set.PairwiseDisjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.instSDiff Set.sUnion	—	Finset.induction Finset.coe_empty Set.sUnion_empty Set.diff_empty Finset.singleton_subset_set_iff Finset.coe_singleton Set.sUnion_singleton Finset.coe_insert Set.mem_insert HasSubset.Subset.trans Set.instIsTransSubset Set.subset_insert subset_disjointOfDiff pairwiseDisjoint_disjointOfDiff sUnion_disjointOfDiff Set.disjoint_of_subset Set.diff_subset Subtype.prop Finset.coe_biUnion Set.iUnion_congr_Prop Set.iUnion_true Set.PairwiseDisjoint.biUnion iSup_congr_Prop Set.PairwiseDisjoint.elim Set.sUnion_eq_biUnion Set.sUnion_insert Set.union_comm Set.diff_diff Set.iUnion_diff Set.iUnion_exists Set.iUnion_comm Set.iUnion_congr Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty
exists_finpartition_diff 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership	Set.instHasSubset SetLike.coe Finset Finset.instSetLike Finpartition.parts ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.instSDiff	—	diff_eq_sUnion' Finset.supIndep_iff_pairwiseDisjoint Finset.sup_id_eq_sSup Set.sSup_eq_sUnion Finpartition.ofErase_parts Mathlib.Tactic.GCongr.rel_imp_rel Set.instIsTransSubset Finset.erase_subset subset_refl Set.instReflSubset
inter_mem 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership	Set.instInter	—	—
isPiSystem 📖	mathematical	MeasureTheory.IsSetSemiring	IsPiSystem	—	inter_mem
isSetRing_supClosure 📖	mathematical	MeasureTheory.IsSetSemiring	MeasureTheory.IsSetRing DFunLike.coe ClosureOperator Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike supClosure Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice	—	subset_supClosure empty_mem supClosed_supClosure Finset.sup'_eq_sup Finset.induction Finset.sup_empty Set.diff_empty Finset.sup_insert Set.sup_eq_union Set.insert_subset_iff Finset.coe_insert Finset.sup_sdiff_right SupClosed.finsetSup_mem diff_mem_supClosure
mem_supClosure_iff 📖	mathematical	MeasureTheory.IsSetSemiring	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 Set.instHasSubset SetLike.coe Finset Finset.instSetLike Finpartition.parts HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	Finset.sup'_eq_sup Finset.induction Finset.sup_empty Set.insert_subset_iff Finset.coe_insert Finset.sup_insert sup_comm eq_or_ne sup_bot_eq DistribLattice.instIsModularLattice Set.disjoint_sdiff_left sdiff_sup_self Finpartition.extend_parts Finpartition.bind_parts Finset.coe_biUnion Set.iUnion₂_subset_iff exists_finpartition_diff Finpartition.sup_parts Finset.sup_id_set_eq_sUnion SupClosed.sSup_mem supClosed_supClosure Finset.finite_toSet subset_supClosure empty_mem HasSubset.Subset.trans Set.instIsTransSubset
notMem_disjointOfDiff 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership	Finset Finset.instMembership disjointOfDiff	—	sUnion_disjointOfDiff Set.subset_sUnion_of_mem disjoint_sdiff_self_right empty_notMem_disjointOfDiff le_rfl
pairwiseDisjoint_biUnion_disjointOfUnion 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike	Set.PairwiseDisjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.iUnion Finset.instMembership disjointOfUnion	—	disjointOfUnion_props
pairwiseDisjoint_disjointOfDiff 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership	Set.PairwiseDisjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe Finset Finset.instSetLike disjointOfDiff	—	diff_eq_sUnion' Finset.coe_sdiff Finset.coe_singleton Set.PairwiseDisjoint.subset Set.diff_subset
pairwiseDisjoint_disjointOfDiffUnion 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership Set.instHasSubset SetLike.coe Finset Finset.instSetLike	Set.PairwiseDisjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice disjointOfDiffUnion	—	exists_disjoint_finset_diff_eq Finset.coe_sdiff Finset.coe_singleton Set.PairwiseDisjoint.subset Set.diff_subset
pairwiseDisjoint_disjointOfUnion 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike	Set.PairwiseDisjoint Finset.partialOrder Finset.instOrderBot disjointOfUnion	—	disjointOfUnion_props
pairwiseDisjoint_disjointOfUnion_of_mem 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike Finset.instMembership	Set.PairwiseDisjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice disjointOfUnion	—	Set.PairwiseDisjoint.subset pairwiseDisjoint_biUnion_disjointOfUnion Set.subset_iUnion₂_of_subset
pairwiseDisjoint_insert_disjointOfDiff 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership	Set.PairwiseDisjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.instInsert SetLike.coe Finset Finset.instSetLike disjointOfDiff	—	pairwiseDisjoint_disjointOfDiff Set.PairwiseDisjoint.insert_of_notMem notMem_disjointOfDiff Disjoint.mono_right Set.subset_sUnion_of_mem disjoint_sUnion_disjointOfDiff
pairwiseDisjoint_union_disjointOfDiffUnion 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership Set.instHasSubset SetLike.coe Finset Finset.instSetLike Set.PairwiseDisjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Set.instUnion disjointOfDiffUnion	—	Set.pairwiseDisjoint_union pairwiseDisjoint_disjointOfDiffUnion Set.disjoint_of_subset Set.subset_sUnion_of_mem disjoint_sUnion_disjointOfDiffUnion
sUnion_disjointOfDiff 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership	Set.sUnion SetLike.coe Finset Finset.instSetLike disjointOfDiff Set.instSDiff	—	diff_eq_sUnion' Finset.coe_sdiff Finset.coe_singleton Set.sUnion_diff_singleton_empty
sUnion_disjointOfDiffUnion_subset 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership Set.instHasSubset SetLike.coe Finset Finset.instSetLike	Set.sUnion disjointOfDiffUnion	—	diff_sUnion_eq_sUnion_disjointOfDiffUnion Set.diff_subset
sUnion_disjointOfUnion 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike	Set.sUnion Set.iUnion Finset.instMembership disjointOfUnion	—	disjointOfUnion_props
sUnion_insert_disjointOfDiff 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership Set.instHasSubset	Set.sUnion Set.instInsert SetLike.coe Finset Finset.instSetLike disjointOfDiff	—	Set.union_diff_cancel sUnion_disjointOfDiff Set.sUnion_insert
sUnion_union_disjointOfDiffUnion_of_subset 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership Set.instHasSubset SetLike.coe Finset Finset.instSetLike	Set.sUnion Finset.instUnion disjointOfDiffUnion	—	sUnion_union_sUnion_disjointOfDiffUnion_of_subset Finset.coe_union Set.sUnion_union
sUnion_union_sUnion_disjointOfDiffUnion_of_subset 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership Set.instHasSubset SetLike.coe Finset Finset.instSetLike	Set.instUnion Set.sUnion disjointOfDiffUnion	—	Set.union_diff_cancel Set.sUnion_subset diff_sUnion_eq_sUnion_disjointOfDiffUnion
subset_disjointOfDiff 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership	Set.instHasSubset SetLike.coe Finset Finset.instSetLike disjointOfDiff	—	diff_eq_sUnion' Finset.coe_sdiff Finset.coe_singleton HasSubset.Subset.trans Set.instIsTransSubset Set.subset_insert
subset_of_diffUnion_disjointOfDiffUnion 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership Set.instHasSubset SetLike.coe Finset Finset.instSetLike disjointOfDiffUnion	Set.instSDiff Set.sUnion	—	Set.sUnion_subset_iff diff_sUnion_eq_sUnion_disjointOfDiffUnion subset_refl Set.instReflSubset
subset_of_mem_disjointOfDiffUnion 📖	—	MeasureTheory.IsSetSemiring Set Set.instMembership Set.instHasSubset SetLike.coe Finset Finset.instSetLike disjointOfDiffUnion	—	—	le_trans subset_of_diffUnion_disjointOfDiffUnion sdiff_le
subset_of_mem_disjointOfUnion 📖	—	MeasureTheory.IsSetSemiring Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike Finset.instMembership disjointOfUnion	—	—	Set.sUnion_subset_iff disjointOfUnion_subset_of_mem

(root)

Definitions

Name	Category	Theorems
SetSemiring 📖	CompOp	30 math math: SetSemiring.instIsOrderedRing, Set.up_union, SetSemiring.mulRightMono, SetSemiring.up_lt_up, SetSemiring.imageHom_def, SetSemiring.down_one, SetSemiring.down_mul, SetSemiring.zero_def, SetSemiring.mulLeftMono, SetSemiring.instCanonicallyOrderedAdd, Set.up_mul, SetSemiring.add_def, Set.up_empty, SetSemiring.one_def, Submodule.singleton_smul, Set.up_image, SetSemiring.down_imageHom, SetSemiring.up_le_up, SetSemiring.down_add, SetSemiring.down_ssubset_down, Set.up_one, SetSemiring.down_subset_down, Submodule.setSemiring_smul_def, SetSemiring.down_up, Submodule.span.ringHom_apply, SetSemiring.mul_def, SetSemiring.instNoZeroDivisors, SetSemiring.down_zero, SetSemiring.up_down, SetSemiring.addLeftMono

---

← Back to Index