Partition

📁 Source: Mathlib/Data/Setoid/Partition.lean

Statistics

Metric	Count
Definitions IndexedPartition, coarserPartition, equivQuotient, index, instInhabitedQuotient, instInhabitedUnivOfUnique, mk', out, piecewise, proj, setoid, some, Partition, Partition, IsPartition, finpartition, completeLattice, le, orderIso, partialOrder, classes, mkClasses, quotientEquivClasses, setoidOfDisjointUnion	24
Theorems isPartition_parts, class_of, disjoint, eq, eq_of_mem, equivQuotient_index, equivQuotient_index_apply, equivQuotient_symm_proj_apply, exists_mem, iUnion, index_out, index_some, mem_iff_index_eq, mem_index, out_proj, piecewise_apply, piecewise_bij, piecewise_inj, piecewise_preimage, proj_eq_iff, proj_fiber, proj_out, proj_some_index, range_piecewise, range_piecewise_subset, some_index, some_mem, isPartition_of_exists_of_ne_empty, finpartition_parts, pairwiseDisjoint, sUnion_eq_univ, card_classes_ker_le, classes_eqv_classes, classes_inj, classes_ker_subset_fiber_set, classes_mkClasses, empty_notMem_classes, eq_eqv_class_of_mem, eq_iff_classes_eq, eq_of_mem_classes, eq_of_mem_eqv_class, eqv_class_mem, eqv_class_mem', eqv_classes_disjoint, eqv_classes_of_disjoint_union, exists_of_mem_partition, finite_classes_ker, isPartition_classes, mem_classes, mkClasses_classes, nonempty_of_mem_partition, quotientEquivClasses_mk_eq, rel_iff_exists_classes, sUnion_classes	54
Total	78

Finpartition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPartition_parts 📖	mathematical	—	Setoid.IsPartition SetLike.coe Finset Set Finset.instSetLike parts ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.univ	—	bot_notMem Setoid.eqv_classes_of_disjoint_union Finset.sup_id_set_eq_sUnion sup_parts Finset.SupIndep.pairwiseDisjoint supIndep

IndexedPartition

Definitions

Name	Category	Theorems
coarserPartition 📖	CompOp	—
equivQuotient 📖	CompOp	4 math math: proj_fiber, equivQuotient_symm_proj_apply, equivQuotient_index_apply, equivQuotient_index
index 📖	CompOp	14 math math: equivQuotient_symm_proj_apply, mem_iff_index_eq, some_index, class_of, equivQuotient_index_apply, index_some, out_proj, proj_eq_iff, piecewise_apply, eq, index_out, mem_index, proj_some_index, equivQuotient_index
instInhabitedQuotient 📖	CompOp	—
instInhabitedUnivOfUnique 📖	CompOp	—
mk' 📖	CompOp	—
out 📖	CompOp	3 math math: proj_out, out_proj, index_out
piecewise 📖	CompOp	10 math math: aestronglyMeasurable_piecewise, piecewise_preimage, piecewise_bij, piecewise_inj, measurable_piecewise, stronglyMeasurable_piecewise, piecewise_apply, aemeasurable_piecewise, range_piecewise, range_piecewise_subset
proj 📖	CompOp	8 math math: proj_fiber, equivQuotient_symm_proj_apply, proj_out, equivQuotient_index_apply, out_proj, proj_eq_iff, proj_some_index, equivQuotient_index
setoid 📖	CompOp	3 math math: some_index, class_of, index_out
some 📖	CompOp	5 math math: some_index, some_mem, index_some, out_proj, proj_some_index

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
class_of 📖	mathematical	—	setOf setoid index	—	Set.ext mem_iff_index_eq
disjoint 📖	mathematical	—	Pairwise Function.onFun Set 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.disjoint_left eq_of_mem
eq 📖	mathematical	—	setOf index	—	Set.ext mem_iff_index_eq
eq_of_mem 📖	—	Set Set.instMembership	—	—	—
equivQuotient_index 📖	mathematical	—	Quotient DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike equivQuotient index proj	—	equivQuotient_index_apply
equivQuotient_index_apply 📖	mathematical	—	DFunLike.coe Equiv Quotient EquivLike.toFunLike Equiv.instEquivLike equivQuotient index proj	—	proj_eq_iff some_index
equivQuotient_symm_proj_apply 📖	mathematical	—	DFunLike.coe Equiv Quotient EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivQuotient proj index	—	—
exists_mem 📖	mathematical	—	Set Set.instMembership	—	mem_index
iUnion 📖	mathematical	—	Set.iUnion Set.univ	—	Set.ext exists_mem
index_out 📖	mathematical	—	index Quotient.out setoid DFunLike.coe Function.Embedding Quotient Function.instFunLikeEmbedding out	—	Quotient.inductionOn' Setoid.ker_apply_mk_out index_some
index_some 📖	mathematical	—	index some	—	mem_iff_index_eq some_mem
mem_iff_index_eq 📖	mathematical	—	Set Set.instMembership index	—	eq_of_mem mem_index
mem_index 📖	mathematical	—	Set Set.instMembership index	—	—
out_proj 📖	mathematical	—	DFunLike.coe Function.Embedding Quotient Function.instFunLikeEmbedding out proj some index	—	—
piecewise_apply 📖	mathematical	—	piecewise index	—	—
piecewise_bij 📖	mathematical	Set.BijOn	Function.Bijective piecewise	—	Set.BijOn.congr piecewise_apply mem_iff_index_eq Set.injOn_of_injective Set.BijOn.injOn Set.BijOn.image_eq disjoint Set.bijOn_univ iUnion Set.bijOn_iUnion
piecewise_inj 📖	mathematical	Set.InjOn Set.PairwiseDisjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.univ Set.image	piecewise	—	Set.PairwiseDisjoint.elim Mathlib.Tactic.Contrapose.contrapose₃ Disjoint.ne_of_mem Set.mem_image_of_mem mem_index
piecewise_preimage 📖	mathematical	—	Set.preimage piecewise Set.iUnion Set Set.instInter	—	Set.ext Set.mem_iUnion_of_mem Set.mem_inter mem_index Set.mem_preimage piecewise_apply mem_iff_index_eq
proj_eq_iff 📖	mathematical	—	proj index	—	Quotient.eq''
proj_fiber 📖	mathematical	—	Set.preimage Quotient proj Set Set.instSingletonSet DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivQuotient	—	Quotient.inductionOn' Set.ext mem_iff_index_eq Quotient.eq''
proj_out 📖	mathematical	—	proj DFunLike.coe Function.Embedding Quotient Function.instFunLikeEmbedding out	—	Quotient.inductionOn' Quotient.sound' some_index
proj_some_index 📖	mathematical	—	proj some index	—	Quotient.eq'' some_index
range_piecewise 📖	mathematical	—	Set.range piecewise Set.iUnion Set.image	—	Set.ext Set.mem_iUnion_of_mem mem_index mem_iff_index_eq
range_piecewise_subset 📖	mathematical	—	Set Set.instHasSubset Set.range piecewise Set.iUnion	—	—
some_index 📖	mathematical	—	setoid some index	—	index_some
some_mem 📖	mathematical	—	Set Set.instMembership some	—	—

Nat

Definitions

Name	Category	Theorems
Partition 📖	CompData	10 math math: Partition.card_restricted_eq_card_countRestricted, Partition.hasProd_powerSeriesMk_card_countRestricted, Partition.powerSeriesMk_card_restricted_eq_tprod, Partition.toFinsuppAntidiag_injective, Partition.powerSeriesMk_card_restricted_eq_powerSeriesMk_card_countRestricted, Partition.hasProd_powerSeriesMk_card_restricted, Partition.powerSeriesMk_card_countRestricted_eq_tprod, Partition.card_odds_eq_card_distincts, Partition.ofComposition_surj, Partition.coeff_genFun

Set.PairwiseDisjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPartition_of_exists_of_ne_empty 📖	mathematical	Set.PairwiseDisjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.instMembership Set.instEmptyCollection	Setoid.IsPartition	—	existsUnique_of_exists_of_unique elim

Setoid

Definitions

Name	Category	Theorems
IsPartition 📖	MathDef	7 math math: Finpartition.isPartition_parts, SimpleGraph.Partition.isPartition, isPartition_classes, Set.PairwiseDisjoint.isPartition_of_exists_of_ne_empty, MulAction.IsPartition.of_orbits, SimpleGraph.Coloring.colorClasses_isPartition, AddAction.IsPartition.of_orbits
classes 📖	CompOp	14 math math: finite_classes_ker, classes_mkClasses, classes_ker_subset_fiber_set, isPartition_classes, mkClasses_classes, classes_eqv_classes, empty_notMem_classes, sUnion_classes, DiscreteQuotient.comp_finsetClopens, classes_inj, card_classes_ker_le, quotientEquivClasses_mk_eq, rel_iff_exists_classes, mem_classes
mkClasses 📖	CompOp	6 math math: classes_mkClasses, mkClasses_classes, eqv_class_mem, eq_eqv_class_of_mem, exists_of_mem_partition, eqv_class_mem'
quotientEquivClasses 📖	CompOp	1 math math: quotientEquivClasses_mk_eq
setoidOfDisjointUnion 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_classes_ker_le 📖	mathematical	—	Fintype.card Set.Elem Set classes ker	—	le_trans Set.card_le_card classes_ker_subset_fiber_set Fintype.card_range_le
classes_eqv_classes 📖	mathematical	—	ExistsUnique Set Set.instMembership classes	—	ExistsUnique.intro mem_classes refl' Set.ext trans' symm'
classes_inj 📖	mathematical	—	classes	—	ext
classes_ker_subset_fiber_set 📖	mathematical	—	Set Set.instHasSubset classes ker Set.range setOf	—	Set.mem_range
classes_mkClasses 📖	mathematical	IsPartition	classes mkClasses Set Set.instMembership Set.instEmptyCollection	—	Set.ext eq_eqv_class_of_mem exists_of_mem_partition
empty_notMem_classes 📖	mathematical	—	Set Set.instMembership classes Set.instEmptyCollection	—	Set.notMem_empty refl'
eq_eqv_class_of_mem 📖	mathematical	ExistsUnique Set Set.instMembership	setOf mkClasses	—	Set.ext eq_of_mem_eqv_class
eq_iff_classes_eq 📖	mathematical	—	setOf	—	ext Set.ext_iff
eq_of_mem_classes 📖	—	Set Set.instMembership classes	—	—	eq_of_mem_eqv_class classes_eqv_classes
eq_of_mem_eqv_class 📖	—	ExistsUnique Set Set.instMembership	—	—	ExistsUnique.unique
eqv_class_mem 📖	mathematical	ExistsUnique Set Set.instMembership	setOf mkClasses	—	ExistsUnique.elim eq_eqv_class_of_mem
eqv_class_mem' 📖	mathematical	ExistsUnique Set Set.instMembership	setOf mkClasses	—	comm' eqv_class_mem
eqv_classes_disjoint 📖	mathematical	ExistsUnique 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.disjoint_left ExistsUnique.elim eq_of_mem_eqv_class
eqv_classes_of_disjoint_union 📖	mathematical	Set.sUnion Set.univ Set.PairwiseDisjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	ExistsUnique Set.instMembership	—	Set.mem_sUnion Set.mem_univ ExistsUnique.intro Set.PairwiseDisjoint.elim_set
exists_of_mem_partition 📖	mathematical	IsPartition Set Set.instMembership	setOf mkClasses Set.instEmptyCollection	—	nonempty_of_mem_partition eq_eqv_class_of_mem
finite_classes_ker 📖	mathematical	—	Set.Finite Set classes ker	—	Set.Finite.subset Set.finite_range classes_ker_subset_fiber_set
isPartition_classes 📖	mathematical	—	IsPartition classes	—	empty_notMem_classes classes_eqv_classes
mem_classes 📖	mathematical	—	Set Set.instMembership classes setOf	—	—
mkClasses_classes 📖	mathematical	—	mkClasses classes classes_eqv_classes	—	ext classes_eqv_classes symm' mem_classes refl' eq_of_mem_classes
nonempty_of_mem_partition 📖	mathematical	IsPartition Set Set.instMembership	Set.Nonempty	—	Set.nonempty_iff_ne_empty
quotientEquivClasses_mk_eq 📖	mathematical	—	Set Set.instMembership classes DFunLike.coe Equiv Set.Elem EquivLike.toFunLike Equiv.instEquivLike quotientEquivClasses setOf	—	mem_classes
rel_iff_exists_classes 📖	mathematical	—	Set Set.instMembership classes	—	mem_classes refl' trans' symm'
sUnion_classes 📖	mathematical	—	Set.sUnion classes Set.univ	—	Set.eq_univ_of_forall Set.mem_sUnion

Setoid.IsPartition

Definitions

Name	Category	Theorems
finpartition 📖	CompOp	1 math math: finpartition_parts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finpartition_parts 📖	mathematical	Setoid.IsPartition SetLike.coe Finset Set Finset.instSetLike	Finpartition.parts ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.univ finpartition	—	—
pairwiseDisjoint 📖	mathematical	Setoid.IsPartition	Set.PairwiseDisjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	Setoid.eqv_classes_disjoint
sUnion_eq_univ 📖	mathematical	Setoid.IsPartition	Set.sUnion Set.univ	—	Set.eq_univ_of_forall Set.mem_sUnion

Setoid.Partition

Definitions

Name	Category	Theorems
completeLattice 📖	CompOp	—
le 📖	CompOp	—
orderIso 📖	CompOp	—
partialOrder 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
IndexedPartition 📖	CompData	—
Partition 📖	CompData	13 math math: Partition.bot_notMem, Partition.pairwiseDisjoint, Partition.coe_copy, Partition.partscopyEquiv_symm_apply_coe, Partition.iSup_eq, Partition.ext_iff, Partition.sSupIndep, Partition.mem_copy_iff, Partition.sSup_eq, Partition.coe_removeBot, Partition.partscopyEquiv_apply_coe, Partition.parts_nonempty, Partition.coe_parts

---

← Back to Index