Documentation Verification Report

Equitabilise

📁 Source: Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean

Statistics

Metric	Count
Definitions `equitabilise`	1
Theorems `card_eq_of_mem_parts_equitabilise`, `card_filter_equitabilise_big`, `card_filter_equitabilise_small`, `card_parts_equitabilise`, `card_parts_equitabilise_subset_le`, `equitabilise_aux`, `equitabilise_isEquipartition`, `exists_equipartition_card_eq`	8
Total	9

Finpartition

Definitions

Name	Category	Theorems
`equitabilise` 📖	CompOp	5 math math: `card_parts_equitabilise_subset_le`, `card_filter_equitabilise_big`, `card_filter_equitabilise_small`, `card_parts_equitabilise`, `equitabilise_isEquipartition`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_eq_of_mem_parts_equitabilise` 📖	—	`Finset.card` `Finset` `Finset.instMembership` `parts` `Finset.instLattice` `Finset.instOrderBot` `equitabilise`	—	—	`equitabilise_aux`
`card_filter_equitabilise_big` 📖	mathematical	`Finset.card`	`Finset` `Finset.filter` `parts` `Finset.instLattice` `Finset.instOrderBot` `equitabilise`	—	`equitabilise_aux`
`card_filter_equitabilise_small` 📖	mathematical	`Finset.card`	`Finset` `Finset.filter` `parts` `Finset.instLattice` `Finset.instOrderBot` `equitabilise`	—	`mul_eq_mul_right_iff` `IsCancelMulZero.toIsRightCancelMulZero` `Nat.instIsCancelMulZero` `AddRightCancelSemigroup.toIsRightCancelAdd` `sum_card_parts` `Finset.filter_or` `Finset.filter_true_of_mem` `card_eq_of_mem_parts_equitabilise` `Finset.sum_union` `Finset.disjoint_filter_filter'` `Finset.sum_const_nat` `Finset.mem_filter` `card_filter_equitabilise_big`
`card_parts_equitabilise` 📖	mathematical	`Finset.card`	`Finset` `parts` `Finset.instLattice` `Finset.instOrderBot` `equitabilise`	—	`Finset.filter_true_of_mem` `card_eq_of_mem_parts_equitabilise` `Finset.filter_or` `Finset.card_union_of_disjoint` `card_filter_equitabilise_small` `card_filter_equitabilise_big`
`card_parts_equitabilise_subset_le` 📖	mathematical	`Finset.card` `Finset` `Finset.instMembership` `parts` `Finset.instLattice` `Finset.instOrderBot`	`Finset.instSDiff` `Finset.biUnion` `Finset.filter` `Finset.instHasSubset` `Finset.instDecidableRelSubset` `equitabilise`	—	`equitabilise_aux`
`equitabilise_aux` 📖	mathematical	`Finset.card`	`Finset` `Finset.instSDiff` `Finset.biUnion` `Finset.filter` `Finset.instHasSubset` `Finset.instDecidableRelSubset` `parts` `Finset.instLattice` `Finset.instOrderBot`	—	`Finset.singleton_injective` `zero_add` `Finset.card_singleton` `Finset.filter.congr_simp` `Finset.mem_map_of_mem` `le` `Finset.singleton_subset_iff` `Finset.mem_singleton_self` `Finset.filter_true_of_mem` `Finset.card_map` `MulZeroClass.mul_zero` `mul_one` `instIsEmptyFalse` `Unique.eq_default` `Finset.filter_empty` `Finset.sdiff_empty` `MulZeroClass.zero_mul` `add_zero` `tsub_mul` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `LE.total` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `covariant_swap_mul_of_covariant_mul` `Nat.instMulLeftMono` `one_mul` `le_add_right` `tsub_add_eq_add_tsub` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.succ_pos'` `le_rfl` `le_add_left` `add_tsub_assoc_of_le` `Finset.exists_subset_card_eq` `LE.le.trans_eq` `Finset.card_pos` `Finset.card_sdiff_of_subset` `Finset.sdiff_ssubset` `DistribLattice.instIsModularLattice` `Finset.Nonempty.ne_empty` `Finset.sdiff_disjoint` `sdiff_sup_cancel` `ite_eq_or_eq` `LE.le.trans` `Finset.card_le_card` `Finset.sdiff_subset` `Finset.filter_insert` `Ne.ite_eq_right_iff` `Finset.card_insert_of_notMem` `le_sdiff_right` `Finset.filter_subset` `tsub_add_cancel_of_le` `Mathlib.Tactic.Push.not_forall_eq` `HasSubset.Subset.trans` `Finset.instIsTransSubset` `Finset.insert_erase` `Finset.biUnion_insert` `eq_or_ne` `Finset.sdiff_eq_empty_iff_subset` `Finset.subset_union_left` `bot_le` `mem_avoid` `LE.le.antisymm` `Finset.sdiff_subset_sdiff` `Finset.Subset.rfl` `Finset.biUnion_subset_biUnion_of_subset_left` `Finset.filter_subset_filter` `Finset.subset_insert` `nonempty_of_mem_parts` `Finset.mem_of_mem_erase` `Disjoint.sdiff_eq_left` `Finset.disjoint_of_subset_right` `disjoint` `Finset.ne_of_mem_erase`
`equitabilise_isEquipartition` 📖	mathematical	`Finset.card`	`IsEquipartition` `equitabilise`	—	`Set.equitableOn_iff_exists_eq_eq_add_one` `card_eq_of_mem_parts_equitabilise`
`exists_equipartition_card_eq` 📖	mathematical	`Finset.card`	`IsEquipartition` `Finset` `parts` `Finset.instLattice` `Finset.instOrderBot`	—	`tsub_mul` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `LE.total` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `covariant_swap_mul_of_covariant_mul` `Nat.instMulLeftMono` `mul_add` `Distrib.leftDistribClass` `add_assoc` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `LT.lt.le` `pos_iff_ne_zero` `mul_one` `add_comm` `Finset.Nonempty.ne_empty` `Finset.card_pos` `LT.lt.trans_le` `equitabilise_isEquipartition` `card_parts_equitabilise` `LT.lt.ne'`

---

← Back to Index