Equipartition

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

Statistics

Metric	Count
Definitions IsEquipartition	1
Theorems average_le_card_part, card_large_parts_eq_mod, card_part_eq_average_iff, card_part_le_average_add_one, card_parts_eq_average, card_small_parts_eq_mod, exists_partPreservingEquiv, exists_partsEquiv, filter_ne_average_add_one_eq_average, bot_isEquipartition, indiscrete_isEquipartition, isEquipartition_iff_card_parts_eq_average, not_isEquipartition, top_isEquipartition, isEquipartition	15
Total	16

Finpartition

Definitions

Name	Category	Theorems
IsEquipartition 📖	MathDef	10 math math: indiscrete_isEquipartition, isEquipartition_iff_card_parts_eq_average, top_isEquipartition, Set.Subsingleton.isEquipartition, exists_equipartition_card_eq, szemeredi_regularity, SimpleGraph.IsTuranMaximal.isEquipartition, equitabilise_isEquipartition, not_isEquipartition, bot_isEquipartition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_isEquipartition 📖	mathematical	—	IsEquipartition Bot.bot Finpartition Finset Finset.instLattice Finset.instOrderBot instBotFinset	—	Set.equitableOn_iff_exists_eq_eq_add_one Finset.singleton_injective Finset.coe_map Set.image_congr Finset.card_singleton Nat.instCharZero Nat.instAtLeastTwoHAddOfNat
indiscrete_isEquipartition 📖	mathematical	—	IsEquipartition indiscrete Finset Finset.instLattice Finset.instOrderBot	—	IsEquipartition.eq_1 indiscrete_parts Finset.coe_singleton Set.equitableOn_singleton IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing
isEquipartition_iff_card_parts_eq_average 📖	mathematical	—	IsEquipartition Finset.card Finset parts Finset.instLattice Finset.instOrderBot	—	sum_card_parts
not_isEquipartition 📖	mathematical	—	IsEquipartition Finset Finset.instMembership parts Finset.instLattice Finset.instOrderBot Finset.card	—	Set.not_equitableOn
top_isEquipartition 📖	mathematical	—	IsEquipartition Top.top Finpartition Finset Finset.instLattice Finset.instOrderBot OrderTop.toTop instLE instOrderTopOfDecidableEqBot	—	Set.Subsingleton.isEquipartition parts_top_subsingleton

Finpartition.IsEquipartition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
average_le_card_part 📖	mathematical	Finpartition.IsEquipartition Finset Finset.instMembership Finpartition.parts Finset.instLattice Finset.instOrderBot	Finset.card	—	Finpartition.sum_card_parts Finset.EquitableOn.le
card_large_parts_eq_mod 📖	mathematical	Finpartition.IsEquipartition	Finset.card Finset Finset.filter Finpartition.parts Finset.instLattice Finset.instOrderBot	—	Finpartition.sum_card_parts AddRightCancelSemigroup.toIsRightCancelAdd add_comm Finset.card_filter_add_card_filter_not mul_one add_mul Distrib.rightDistribClass add_assoc mul_add Distrib.leftDistribClass filter_ne_average_add_one_eq_average Finset.sum_const_nat Finset.sum_filter_add_sum_filter_not
card_part_eq_average_iff 📖	mathematical	Finpartition.IsEquipartition Finset Finset.instMembership Finpartition.parts Finset.instLattice Finset.instOrderBot	Finset.card	—	card_parts_eq_average
card_part_le_average_add_one 📖	mathematical	Finpartition.IsEquipartition Finset Finset.instMembership Finpartition.parts Finset.instLattice Finset.instOrderBot	Finset.card	—	Finpartition.sum_card_parts Finset.EquitableOn.le_add_one
card_parts_eq_average 📖	mathematical	Finpartition.IsEquipartition Finset Finset.instMembership Finpartition.parts Finset.instLattice Finset.instOrderBot	Finset.card	—	Finpartition.isEquipartition_iff_card_parts_eq_average
card_small_parts_eq_mod 📖	mathematical	Finpartition.IsEquipartition	Finset.card Finset Finset.filter Finpartition.parts Finset.instLattice Finset.instOrderBot	—	Finset.card_filter_add_card_filter_not card_large_parts_eq_mod add_tsub_cancel_left Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid filter_ne_average_add_one_eq_average
exists_partPreservingEquiv 📖	mathematical	Finpartition.IsEquipartition	Finpartition.part Finset SetLike.instMembership Finset.instSetLike Finset.card DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Finpartition.parts Finset.instLattice Finset.instOrderBot	—	Finpartition.exists_enumeration exists_partsEquiv card_parts_eq_average mul_add_one Distrib.leftDistribClass add_lt_add_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid mul_le_mul_right Nat.instMulLeftMono add_lt_add_of_le_of_lt covariant_swap_add_of_covariant_add Fintype.bijective_iff_injective_and_card LT.lt.ne' LE.le.trans_lt Equiv.injective Fin.heq_ext_iff mul_comm Fintype.card_coe Fintype.card_fin Equiv.apply_eq_iff_eq
exists_partsEquiv 📖	mathematical	Finpartition.IsEquipartition	Finset.card Finset SetLike.instMembership Finset.instSetLike Finpartition.parts Finset.instLattice Finset.instOrderBot DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	card_part_eq_average_iff card_large_parts_eq_mod card_small_parts_eq_mod Finpartition.card_mod_card_parts_le Equiv.sumCompl_symm_apply_of_pos Equiv.sumCompl_symm_apply_of_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd
filter_ne_average_add_one_eq_average 📖	mathematical	Finpartition.IsEquipartition	Finset.filter Finset Finset.card Finpartition.parts Finset.instLattice Finset.instOrderBot	—	Finset.ext card_part_eq_average_iff

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isEquipartition 📖	mathematical	Set.Subsingleton Finset SetLike.coe Finset.instSetLike Finpartition.parts Finset.instLattice Finset.instOrderBot	Finpartition.IsEquipartition	—	equitableOn IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing

---

← Back to Index