Documentation Verification Report

Equitable

📁 Source: Mathlib/Data/Set/Equitable.lean

Statistics

Metric	Count
Definitions `EquitableOn`	1
Theorems `le`, `le_add_one`, `equitableOn_iff`, `equitableOn_iff_le_le_add_one`, `equitableOn`, `equitableOn_empty`, `equitableOn_iff_exists_eq_eq_add_one`, `equitableOn_iff_exists_image_subset_icc`, `equitableOn_iff_exists_le_le_add_one`, `equitableOn_singleton`, `not_equitableOn`	11
Total	12

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equitableOn_iff` 📖	mathematical	—	`Set.EquitableOn` `Nat.instOne` `SetLike.coe` `Finset` `instSetLike` `sum` `Nat.instAddCommMonoid` `card`	—	—
`equitableOn_iff_le_le_add_one` 📖	mathematical	—	`Set.EquitableOn` `Nat.instOne` `SetLike.coe` `Finset` `instSetLike` `sum` `Nat.instAddCommMonoid` `card`	—	`Set.equitableOn_iff_exists_le_le_add_one` `sum_const_nat` `card_pos` `le_rfl` `Mathlib.Tactic.Push.not_forall_eq` `le_trans` `sum_const` `mul_comm` `sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `LT.lt.trans_le` `sum_lt_sum` `Nat.instIsOrderedCancelAddMonoid` `LE.le.lt_of_ne` `le_refl`

Finset.EquitableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le` 📖	mathematical	`Set.EquitableOn` `Nat.instOne` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.instMembership`	`Finset.sum` `Nat.instAddCommMonoid` `Finset.card`	—	`Finset.equitableOn_iff_le_le_add_one`
`le_add_one` 📖	mathematical	`Set.EquitableOn` `Nat.instOne` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.instMembership`	`Finset.sum` `Nat.instAddCommMonoid` `Finset.card`	—	`Finset.equitableOn_iff_le_le_add_one`

Set

Definitions

Name	Category	Theorems
`EquitableOn` 📖	MathDef	9 math math: `Finset.equitableOn_iff_le_le_add_one`, `equitableOn_iff_exists_le_le_add_one`, `equitableOn_singleton`, `Subsingleton.equitableOn`, `Finset.equitableOn_iff`, `equitableOn_empty`, `not_equitableOn`, `equitableOn_iff_exists_eq_eq_add_one`, `equitableOn_iff_exists_image_subset_icc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equitableOn_empty` 📖	mathematical	—	`EquitableOn` `Set` `instEmptyCollection`	—	`notMem_empty`
`equitableOn_iff_exists_eq_eq_add_one` 📖	mathematical	—	`EquitableOn` `Nat.instOne`	—	—
`equitableOn_iff_exists_image_subset_icc` 📖	mathematical	—	`EquitableOn` `Nat.instOne` `Set` `instHasSubset` `image` `Icc` `Nat.instPreorder`	—	`equitableOn_iff_exists_le_le_add_one`
`equitableOn_iff_exists_le_le_add_one` 📖	mathematical	—	`EquitableOn` `Nat.instOne`	—	`eq_empty_or_nonempty` `instIsEmptyFalse` `Mathlib.Tactic.Push.not_forall_eq` `LE.le.antisymm` `le_imp_le_of_le_of_le` `le_refl` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`equitableOn_singleton` 📖	mathematical	—	`EquitableOn` `Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Set` `instSingletonSet`	—	`Subsingleton.equitableOn` `subsingleton_singleton`
`not_equitableOn` 📖	mathematical	—	`EquitableOn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `instMembership` `Preorder.toLT`	—	—

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equitableOn` 📖	mathematical	`Set.Subsingleton`	`Set.EquitableOn` `Preorder.toLE` `PartialOrder.toPreorder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`le_add_of_nonneg_right` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `zero_le_one` `IsOrderedRing.toZeroLEOneClass`

---

← Back to Index