Finpartition

📁 Source: Mathlib/Order/Partition/Finpartition.lean

Statistics

Metric	Count
Definitions `Finpartition`, `atomise`, `avoid`, `bind`, `combine`, `copy`, `empty`, `equivSigmaParts`, `extend`, `extendOfLE`, `indiscrete`, `instBotFinset`, `instFintypeFinset`, `instFintypeOfDecidableEq`, `instInhabitedBot`, `instLE`, `instMin`, `instOrderBotFinset`, `instOrderTopOfDecidableEqBot`, `instPartialOrder`, `instSemilatticeInf`, `instUniqueBot`, `map`, `ofErase`, `ofExistsUnique`, `ofSetSetoid`, `ofSetoid`, `ofSubset`, `part`, `parts`, `restrict`, `uniqueFinpartition`, `instDecidableEqFinpartition`, `decEq`	34
Theorems `atomise_empty`, `avoid_parts_val`, `biUnion_filter_atomise`, `biUnion_parts`, `bind_parts`, `bot_notMem`, `card_atomise_le`, `card_bind`, `card_bot`, `card_extend`, `card_filter_atomise_le_two_pow`, `card_mod_card_parts_le`, `card_mono`, `card_parts_le_card`, `combine_parts`, `copy_parts`, `default_eq_empty`, `disjoint`, `empty_notMem_parts`, `empty_parts`, `eq_of_mem_parts`, `existsUnique_mem`, `exists_enumeration`, `exists_le_of_le`, `exists_mem`, `exists_subset_part_bijOn`, `ext`, `ext_iff`, `extend_parts`, `indiscrete_parts`, `instNonempty`, `le`, `mem_atomise`, `mem_avoid`, `mem_bind`, `mem_bot_iff`, `mem_part`, `mem_part_iff_exists`, `mem_part_iff_part_eq_part`, `mem_part_ofSetSetoid_iff_rel`, `mem_part_ofSetoid_iff_rel`, `mem_part_self`, `ne_bot`, `ne_empty`, `nonempty_of_mem_parts`, `ofErase_parts`, `ofExistsUnique_parts`, `ofSetSetoid_parts`, `ofSetoid_parts_val`, `ofSubset_parts`, `part_eq_empty`, `part_eq_iff_mem`, `part_eq_of_mem`, `part_mem`, `part_nonempty`, `part_subset`, `part_surjOn`, `parts_bot`, `parts_eq_empty_iff`, `parts_extendOfLE_of_eq`, `parts_extendOfLE_of_lt`, `parts_inf`, `parts_map`, `parts_nonempty`, `parts_nonempty_iff`, `parts_subset_extendOfLE`, `parts_top_subset`, `parts_top_subsingleton`, `subset`, `sum_card_parts`, `sum_combine`, `sum_restrict`, `supIndep`, `sup_parts`	74
Total	108

Finpartition

Definitions

Name	Category	Theorems
`atomise` 📖	CompOp	5 math math: `mem_atomise`, `card_atomise_le`, `card_filter_atomise_le_two_pow`, `biUnion_filter_atomise`, `atomise_empty`
`avoid` 📖	CompOp	2 math math: `mem_avoid`, `avoid_parts_val`
`bind` 📖	CompOp	3 math math: `bind_parts`, `card_bind`, `mem_bind`
`combine` 📖	CompOp	2 math math: `combine_parts`, `sum_combine`
`copy` 📖	CompOp	1 math math: `copy_parts`
`empty` 📖	CompOp	2 math math: `empty_parts`, `default_eq_empty`
`equivSigmaParts` 📖	CompOp	—
`extend` 📖	CompOp	2 math math: `extend_parts`, `card_extend`
`extendOfLE` 📖	CompOp	3 math math: `parts_subset_extendOfLE`, `parts_extendOfLE_of_lt`, `parts_extendOfLE_of_eq`
`indiscrete` 📖	CompOp	2 math math: `indiscrete_isEquipartition`, `indiscrete_parts`
`instBotFinset` 📖	CompOp	6 math math: `parts_bot`, `bot_isUniform`, `mem_bot_iff`, `card_bot`, `nonUniforms_bot`, `bot_isEquipartition`
`instFintypeFinset` 📖	CompOp	—
`instFintypeOfDecidableEq` 📖	CompOp	—
`instInhabitedBot` 📖	CompOp	1 math math: `default_eq_empty`
`instLE` 📖	CompOp	3 math math: `top_isEquipartition`, `parts_top_subset`, `parts_top_subsingleton`
`instMin` 📖	CompOp	1 math math: `parts_inf`
`instOrderBotFinset` 📖	CompOp	—
`instOrderTopOfDecidableEqBot` 📖	CompOp	3 math math: `top_isEquipartition`, `parts_top_subset`, `parts_top_subsingleton`
`instPartialOrder` 📖	CompOp	—
`instSemilatticeInf` 📖	CompOp	—
`instUniqueBot` 📖	CompOp	—
`map` 📖	CompOp	1 math math: `parts_map`
`ofErase` 📖	CompOp	1 math math: `ofErase_parts`
`ofExistsUnique` 📖	CompOp	1 math math: `ofExistsUnique_parts`
`ofSetSetoid` 📖	CompOp	2 math math: `mem_part_ofSetSetoid_iff_rel`, `ofSetSetoid_parts`
`ofSetoid` 📖	CompOp	2 math math: `mem_part_ofSetoid_iff_rel`, `ofSetoid_parts_val`
`ofSubset` 📖	CompOp	1 math math: `ofSubset_parts`
`part` 📖	CompOp	18 math math: `mem_part_ofSetSetoid_iff_rel`, `SimpleGraph.IsTuranMaximal.not_adj_iff_part_eq`, `mem_part_iff_part_eq_part`, `part_eq_of_mem`, `part_eq_empty`, `mem_part_ofSetoid_iff_rel`, `part_mem`, `exists_enumeration`, `mem_part_iff_exists`, `part_nonempty`, `mem_part_self`, `part_subset`, `part_eq_iff_mem`, `SimpleGraph.IsTuranMaximal.degree_eq_card_sub_part_card`, `IsEquipartition.exists_partPreservingEquiv`, `part_surjOn`, `exists_subset_part_bijOn`, `mem_part`
`parts` 📖	CompOp	92 math math: `ofExistsUnique_parts`, `empty_parts`, `IsEquipartition.filter_ne_average_add_one_eq_average`, `isPartition_parts`, `combine_parts`, `equitabilise_aux`, `SzemerediRegularity.a_add_one_le_four_pow_parts_card`, `parts_subset_extendOfLE`, `card_filter_equitabilise_big`, `IsEquipartition.card_biUnion_offDiag_le'`, `SimpleGraph.regularityReduced_adj`, `IsEquipartition.card_large_parts_eq_mod`, `disjoint`, `parts_bot`, `mk_mem_nonUniforms`, `Rel.card_interedges_finpartition`, `isEquipartition_iff_card_parts_eq_average`, `mem_avoid`, `parts_map`, `ofErase_parts`, `card_parts_le_card`, `indiscrete_parts`, `sum_restrict`, `extend_parts`, `MeasureTheory.IsSetSemiring.mem_supClosure_iff`, `parts_top_subset`, `Setoid.IsPartition.finpartition_parts`, `card_nonuniformWitnesses_le`, `SimpleGraph.IsTuranMaximal.card_parts_le`, `Rel.card_interedges_finpartition_right`, `IsEquipartition.sum_nonUniforms_lt'`, `exists_mem`, `parts_eq_empty_iff`, `parts_extendOfLE_of_lt`, `bind_parts`, `mem_atomise`, `IsEquipartition.card_small_parts_eq_mod`, `parts_nonempty_iff`, `part_mem`, `exists_enumeration`, `mem_part_iff_exists`, `ext_iff`, `exists_equipartition_card_eq`, `card_atomise_le`, `szemeredi_regularity`, `coe_energy`, `biUnion_parts`, `empty_notMem_parts`, `card_mod_card_parts_le`, `SimpleGraph.unreduced_edges_subset`, `copy_parts`, `mem_bot_iff`, `card_bind`, `MeasureTheory.preVariation.sum_le`, `MeasureTheory.preVariation.sum_le_preVariationFun_iUnion'`, `ofSetoid_parts_val`, `card_filter_atomise_le_two_pow`, `mem_bind`, `nonempty_of_not_uniform`, `existsUnique_mem`, `card_filter_equitabilise_small`, `card_bot`, `MeasureTheory.preVariation.exists_Finpartition_sum_ge`, `MeasureTheory.preVariation.exists_Finpartition_sum_gt`, `card_mono`, `card_parts_equitabilise`, `SimpleGraph.IsTuranMaximal.card_parts`, `mk_mem_sparsePairs`, `IsEquipartition.exists_partsEquiv`, `Rel.card_interedges_finpartition_left`, `SzemerediRegularity.coe_m_add_one_pos`, `supIndep`, `parts_top_subsingleton`, `sum_card_parts`, `bot_notMem`, `card_extend`, `IsEquipartition.exists_partPreservingEquiv`, `biUnion_filter_atomise`, `MeasureTheory.IsSetSemiring.exists_finpartition_diff`, `sup_parts`, `parts_extendOfLE_of_eq`, `MeasureTheory.preVariation.sum_le_preVariationFun_of_subset`, `parts_nonempty`, `sum_combine`, `not_isEquipartition`, `part_surjOn`, `exists_subset_part_bijOn`, `parts_inf`, `avoid_parts_val`, `IsEquipartition.card_interedges_sparsePairs_le'`, `atomise_empty`, `ofSetSetoid_parts`
`restrict` 📖	CompOp	1 math math: `sum_restrict`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`atomise_empty` 📖	mathematical	`Finset.Nonempty`	`parts` `Finset` `Finset.instLattice` `Finset.instOrderBot` `atomise` `Finset.instEmptyCollection` `Finset.instSingleton`	—	`Finset.filter.congr_simp` `instIsEmptyFalse` `Finset.filter_true` `Finset.image_singleton` `ofErase.congr_simp` `Finset.erase_eq_of_notMem` `Finset.notMem_singleton` `Finset.Nonempty.ne_empty`
`avoid_parts_val` 📖	mathematical	—	`Finset.val` `parts` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toOrderBot` `GeneralizedBooleanAlgebra.toSDiff` `avoid` `Multiset.erase` `Multiset.dedup` `Multiset.map` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	—
`biUnion_filter_atomise` 📖	mathematical	`Finset` `Finset.instMembership` `Finset.instHasSubset`	`Finset.biUnion` `Finset.filter` `Finset.Nonempty` `Finset.instDecidableRelSubset` `Finset.decidableNonempty` `parts` `Finset.instLattice` `Finset.instOrderBot` `atomise`	—	`Finset.ext` `Finset.mem_biUnion` `Finset.mem_filter` `exists_mem` `mem_atomise`
`biUnion_parts` 📖	mathematical	—	`Finset.biUnion` `Finset` `parts` `Finset.instLattice` `Finset.instOrderBot`	—	`Finset.sup_eq_biUnion` `sup_parts`
`bind_parts` 📖	mathematical	—	`parts` `bind` `Finset.biUnion` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.attach`	—	—
`bot_notMem` 📖	mathematical	—	`Finset` `Finset.instMembership` `parts` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	—
`card_atomise_le` 📖	mathematical	—	`Finset.card` `Finset` `parts` `Finset.instLattice` `Finset.instOrderBot` `atomise` `Monoid.toNatPow` `Nat.instMonoid`	—	`LE.le.trans` `Finset.card_le_card` `Finset.erase_subset` `Finset.card_image_le` `Eq.le` `Finset.card_powerset`
`card_bind` 📖	mathematical	—	`Finset.card` `parts` `bind` `Finset.sum` `Finset` `Finset.instMembership` `Nat.instAddCommMonoid` `Finset.attach`	—	`Finset.card_biUnion` `Function.onFun.eq_1` `Finset.disjoint_left` `ne_bot` `eq_bot_iff` `LE.le.trans` `le_inf` `le` `Disjoint.le_bot` `disjoint`
`card_bot` 📖	mathematical	—	`Finset.card` `Finset` `parts` `Finset.instLattice` `Finset.instOrderBot` `Bot.bot` `Finpartition` `instBotFinset`	—	`Finset.card_map` `Finset.singleton_injective`
`card_extend` 📖	mathematical	`Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	`Finset.card` `parts` `extend`	—	`Finset.card_insert_of_notMem` `Disjoint.eq_bot_of_le` `Disjoint.symm` `le`
`card_filter_atomise_le_two_pow` 📖	mathematical	`Finset` `Finset.instMembership`	`Finset.card` `Finset.filter` `Finset.instHasSubset` `Finset.Nonempty` `Finset.instDecidableRelSubset` `Finset.decidableNonempty` `parts` `Finset.instLattice` `Finset.instOrderBot` `atomise` `Monoid.toNatPow` `Nat.instMonoid`	—	`Finset.subset_iff` `Finset.erase_subset_erase` `Finset.filter.congr_simp` `Finset.insert_erase` `Finset.mem_filter` `LE.le.trans` `Finset.card_le_card` `Finset.card_image_le` `Finset.card_powerset` `Finset.card_erase_of_mem` `le_refl`
`card_mod_card_parts_le` 📖	mathematical	—	`Finset.card` `Finset` `parts` `Finset.instLattice` `Finset.instOrderBot`	—	`Finset.card_eq_zero` `Finset.bot_eq_empty` `parts_eq_empty_iff` `le_refl` `LT.lt.le`
`card_mono` 📖	mathematical	`Finpartition` `instLE`	`Finset.card` `parts`	—	`exists_le_of_le` `Finset.card_attach` `Finset.card_le_card_of_injOn` `Subtype.coe_injective` `Set.PairwiseDisjoint.elim` `disjoint` `ne_bot` `disjoint_self` `Disjoint.mono` `LE.le.trans` `Eq.le`
`card_parts_le_card` 📖	mathematical	—	`Finset.card` `Finset` `parts` `Finset.instLattice` `Finset.instOrderBot`	—	`card_bot` `card_mono` `bot_le`
`combine_parts` 📖	mathematical	`Finset.SupIndep`	`parts` `Finset.sup` `Lattice.toSemilatticeSup` `combine` `Finset.biUnion`	—	—
`copy_parts` 📖	mathematical	—	`parts` `copy`	—	—
`default_eq_empty` 📖	mathematical	—	`Finpartition` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instInhabitedBot` `empty`	—	—
`disjoint` 📖	mathematical	—	`Set.PairwiseDisjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `SetLike.coe` `Finset` `Finset.instSetLike` `parts`	—	`Finset.SupIndep.pairwiseDisjoint` `supIndep`
`empty_notMem_parts` 📖	mathematical	—	`Finset` `Finset.instMembership` `parts` `Finset.instLattice` `Finset.instOrderBot` `Finset.instEmptyCollection`	—	`bot_notMem`
`empty_parts` 📖	mathematical	—	`parts` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `empty` `Finset` `Finset.instEmptyCollection`	—	—
`eq_of_mem_parts` 📖	—	`Finset` `Finset.instMembership` `parts` `Finset.instLattice` `Finset.instOrderBot`	—	—	`Set.PairwiseDisjoint.elim` `disjoint` `Finset.not_disjoint_iff`
`existsUnique_mem` 📖	mathematical	`Finset` `Finset.instMembership`	`ExistsUnique` `parts` `Finset.instLattice` `Finset.instOrderBot`	—	`exists_mem` `eq_of_mem_parts`
`exists_enumeration` 📖	mathematical	—	`part` `Finset` `SetLike.instMembership` `Finset.instSetLike` `parts` `Finset.instLattice` `Finset.instOrderBot` `Finset.card` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`Sigma.eta`
`exists_le_of_le` 📖	mathematical	`Finpartition` `instLE` `Finset` `Finset.instMembership` `parts`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	`ne_bot` `disjoint_self` `Disjoint.mono_right` `le` `sup_parts` `Disjoint.mono` `le_refl` `supIndep` `Finset.erase_subset` `Finset.notMem_erase`
`exists_mem` 📖	mathematical	`Finset` `Finset.instMembership`	`parts` `Finset.instLattice` `Finset.instOrderBot`	—	`Finset.mem_sup` `sup_parts`
`exists_subset_part_bijOn` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `Set.BijOn` `part` `SetLike.coe` `Finset.instSetLike` `parts` `Finset.instLattice` `Finset.instOrderBot`	—	`Set.SurjOn.exists_bijOn_subset` `part_surjOn` `CanLift.prf` `Set.instCanLiftFinsetCoeFinite` `Set.Finite.subset` `Finset.finite_toSet` `instIsConcreteLE`
`ext` 📖	—	`parts`	—	—	—
`ext_iff` 📖	mathematical	—	`parts`	—	`ext`
`extend_parts` 📖	mathematical	`Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	`parts` `extend` `Finset` `Finset.instInsert`	—	—
`indiscrete_parts` 📖	mathematical	—	`parts` `indiscrete` `Finset` `Finset.instSingleton`	—	—
`instNonempty` 📖	mathematical	—	`Finpartition`	—	—
`le` 📖	mathematical	`Finset` `Finset.instMembership` `parts`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	`LE.le.trans` `Finset.le_sup` `Eq.le` `sup_parts`
`mem_atomise` 📖	mathematical	—	`Finset` `Finset.instMembership` `parts` `Finset.instLattice` `Finset.instOrderBot` `atomise` `Finset.Nonempty` `Finset.instHasSubset` `Finset.filter` `Finset.decidableDforallFinset`	—	—
`mem_avoid` 📖	mathematical	—	`Finset` `Finset.instMembership` `parts` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toOrderBot` `GeneralizedBooleanAlgebra.toSDiff` `avoid` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	`sdiff_eq_bot_iff`
`mem_bind` 📖	mathematical	—	`Finset` `Finset.instMembership` `parts` `bind`	—	`bind_parts` `Finset.mem_biUnion` `Finset.mem_attach`
`mem_bot_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `parts` `Finset.instLattice` `Finset.instOrderBot` `Bot.bot` `Finpartition` `instBotFinset` `Finset.instSingleton`	—	`Finset.mem_map` `Finset.singleton_injective`
`mem_part` 📖	mathematical	`Finset` `Finset.instMembership`	`part`	—	`mem_part_self`
`mem_part_iff_exists` 📖	mathematical	—	`Finset` `Finset.instMembership` `part` `parts` `Finset.instLattice` `Finset.instOrderBot`	—	`part_nonempty` `part_eq_of_mem`
`mem_part_iff_part_eq_part` 📖	mathematical	`Finset` `Finset.instMembership`	`part`	—	`part_eq_of_mem` `part_mem` `mem_part`
`mem_part_ofSetSetoid_iff_rel` 📖	mathematical	—	`Finset` `Finset.instMembership` `part` `ofSetSetoid`	—	`Setoid.trans'` `Setoid.symm'`
`mem_part_ofSetoid_iff_rel` 📖	mathematical	—	`Finset` `Finset.instMembership` `part` `Finset.univ` `ofSetoid`	—	`mem_part_ofSetSetoid_iff_rel`
`mem_part_self` 📖	mathematical	—	`Finset` `Finset.instMembership` `part`	—	`existsUnique_mem` `Finset.choose_property` `part_eq_empty`
`ne_bot` 📖	—	`Finset` `Finset.instMembership` `parts`	—	—	`bot_notMem`
`ne_empty` 📖	—	`Finset` `Finset.instMembership` `parts` `Finset.instLattice` `Finset.instOrderBot`	—	—	`ne_bot`
`nonempty_of_mem_parts` 📖	mathematical	`Finset` `Finset.instMembership` `parts` `Finset.instLattice` `Finset.instOrderBot`	`Finset.Nonempty`	—	`Finset.nonempty_iff_ne_empty` `ne_bot`
`ofErase_parts` 📖	mathematical	`Finset.SupIndep` `Finset.sup` `Lattice.toSemilatticeSup`	`parts` `ofErase` `Finset.erase` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	—
`ofExistsUnique_parts` 📖	mathematical	`Finset` `Finset.instHasSubset` `ExistsUnique` `Finset.instMembership` `Finset.instEmptyCollection`	`parts` `Finset.instLattice` `Finset.instOrderBot` `ofExistsUnique`	—	—
`ofSetSetoid_parts` 📖	mathematical	—	`parts` `Finset` `Finset.instLattice` `Finset.instOrderBot` `ofSetSetoid` `Finset.image` `Finset.decidableEq` `Finset.filter`	—	—
`ofSetoid_parts_val` 📖	mathematical	—	`Finset.val` `Finset` `parts` `Finset.instLattice` `Finset.instOrderBot` `Finset.univ` `ofSetoid` `Multiset.dedup` `Finset.decidableEq` `Multiset.map` `Finset.filter`	—	—
`ofSubset_parts` 📖	mathematical	`Finset` `Finset.instHasSubset` `parts` `Finset.sup` `Lattice.toSemilatticeSup`	`ofSubset`	—	—
`part_eq_empty` 📖	mathematical	—	`part` `Finset` `Finset.instEmptyCollection` `Finset.instMembership`	—	`ne_empty` `part_mem` `existsUnique_mem`
`part_eq_iff_mem` 📖	mathematical	`Finset` `Finset.instMembership` `parts` `Finset.instLattice` `Finset.instOrderBot`	`part`	—	`eq_of_mem_parts` `le`
`part_eq_of_mem` 📖	mathematical	`Finset` `Finset.instMembership` `parts` `Finset.instLattice` `Finset.instOrderBot`	`part`	—	`part_eq_iff_mem`
`part_mem` 📖	mathematical	—	`Finset` `Finset.instMembership` `parts` `Finset.instLattice` `Finset.instOrderBot` `part`	—	`existsUnique_mem`
`part_nonempty` 📖	mathematical	—	`Finset.Nonempty` `part` `Finset` `Finset.instMembership`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₁` `part_eq_empty`
`part_subset` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `part`	—	`le` `part_mem` `part_eq_empty`
`part_surjOn` 📖	mathematical	—	`Set.SurjOn` `Finset` `part` `SetLike.coe` `Finset.instSetLike` `parts` `Finset.instLattice` `Finset.instOrderBot`	—	`nonempty_of_mem_parts` `Finset.mem_of_subset` `le` `ExistsUnique.unique` `existsUnique_mem` `part_mem` `mem_part`
`parts_bot` 📖	mathematical	—	`parts` `Finset` `Finset.instLattice` `Finset.instOrderBot` `Bot.bot` `Finpartition` `instBotFinset` `Finset.map` `Finset.instSingleton` `Finset.singleton_injective`	—	—
`parts_eq_empty_iff` 📖	mathematical	—	`parts` `Finset` `Finset.instEmptyCollection` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	`sup_parts` `Finset.sup_empty` `Finset.eq_empty_iff_forall_notMem` `bot_notMem` `le_bot_iff` `LE.le.trans` `Finset.le_sup` `Eq.le`
`parts_extendOfLE_of_eq` 📖	mathematical	—	`parts` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra` `GeneralizedBooleanAlgebra.toOrderBot` `extendOfLE` `Eq.le` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	`Eq.le` `disjoint_sdiff_self_right` `sdiff_self`
`parts_extendOfLE_of_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	`parts` `GeneralizedBooleanAlgebra.toOrderBot` `extendOfLE` `le_of_lt` `Finset` `Finset.instInsert` `GeneralizedBooleanAlgebra.toSDiff`	—	`le_of_lt` `Iff.not` `sdiff_eq_bot_iff` `not_le_of_gt` `disjoint_sdiff_self_right`
`parts_inf` 📖	mathematical	—	`parts` `DistribLattice.toLattice` `Finpartition` `instMin` `Finset.erase` `Finset.image` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `SProd.sprod` `Finset` `Finset.instSProd` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	—	—
`parts_map` 📖	mathematical	—	`parts` `DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instFunLikeOrderIso` `map` `Finset.map` `Equiv.toEmbedding` `EquivLike.toEquiv` `OrderIso.instEquivLike`	—	—
`parts_nonempty` 📖	mathematical	—	`Finset.Nonempty` `parts`	—	`parts_nonempty_iff`
`parts_nonempty_iff` 📖	mathematical	—	`Finset.Nonempty` `parts`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₃` `parts_eq_empty_iff`
`parts_subset_extendOfLE` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra`	`Finset` `Finset.instHasSubset` `parts` `GeneralizedBooleanAlgebra.toOrderBot` `extendOfLE`	—	`disjoint_sdiff_self_right` `le_antisymm` `sdiff_eq_bot_iff` `subset_refl` `Finset.instReflSubset` `Finset.subset_insert`
`parts_top_subset` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `parts` `Top.top` `Finpartition` `OrderTop.toTop` `instLE` `instOrderTopOfDecidableEqBot` `Finset.instSingleton`	—	—
`parts_top_subsingleton` 📖	mathematical	—	`Set.Subsingleton` `SetLike.coe` `Finset` `Finset.instSetLike` `parts` `Top.top` `Finpartition` `OrderTop.toTop` `instLE` `instOrderTopOfDecidableEqBot`	—	`Set.subsingleton_of_subset_singleton` `Finset.mem_singleton` `parts_top_subset`
`subset` 📖	mathematical	`Finset` `Finset.instMembership` `parts` `Finset.instLattice` `Finset.instOrderBot`	`Finset.instHasSubset`	—	`le`
`sum_card_parts` 📖	mathematical	—	`Finset.sum` `Finset` `Nat.instAddCommMonoid` `parts` `Finset.instLattice` `Finset.instOrderBot` `Finset.card`	—	`Finset.card_biUnion` `Finset.SupIndep.pairwiseDisjoint` `supIndep` `biUnion_parts`
`sum_combine` 📖	mathematical	`Finset.SupIndep`	`Finset.sum` `parts` `Finset.sup` `Lattice.toSemilatticeSup` `combine`	—	`Finset.sum_biUnion` `Function.onFun.eq_1` `Finset.disjoint_left` `Disjoint.mono` `le` `Finset.SupIndep.pairwiseDisjoint` `ne_bot` `disjoint_self`
`sum_restrict` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `Bot.bot` `OrderBot.toBot` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Finset.sum` `parts` `restrict` `SemilatticeInf.toMin`	—	`Disjoint.mono` `inf_le_left` `disjoint` `Finset.sum_eq_zero` `Finset.filter.congr_simp` `Finset.sum_congr` `Finset.sum_image` `Finset.sum_filter_add_sum_filter_not` `add_zero`
`supIndep` 📖	mathematical	—	`Finset.SupIndep` `parts`	—	—
`sup_parts` 📖	mathematical	—	`Finset.sup` `Lattice.toSemilatticeSup` `parts`	—	—

IsAtom

Definitions

Name	Category	Theorems
`uniqueFinpartition` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`Finpartition` 📖	CompData	12 math math: `Finpartition.parts_bot`, `Finpartition.bot_isUniform`, `Finpartition.top_isEquipartition`, `Finpartition.parts_top_subset`, `Finpartition.default_eq_empty`, `Finpartition.mem_bot_iff`, `Finpartition.card_bot`, `Finpartition.instNonempty`, `Finpartition.nonUniforms_bot`, `Finpartition.parts_top_subsingleton`, `Finpartition.bot_isEquipartition`, `Finpartition.parts_inf`
`instDecidableEqFinpartition` 📖	CompOp	—

instDecidableEqFinpartition

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

---

← Back to Index