Documentation Verification Report

Pigeonhole

📁 Source: Mathlib/Combinatorics/Pigeonhole.lean

Statistics

Metric	Count
Definitions	0
Theorems `exists_card_fiber_le_of_card_le_mul`, `exists_card_fiber_le_of_card_le_nsmul`, `exists_card_fiber_lt_of_card_lt_mul`, `exists_card_fiber_lt_of_card_lt_nsmul`, `exists_le_card_fiber_of_mul_le_card_of_maps_to`, `exists_le_card_fiber_of_nsmul_le_card_of_maps_to`, `exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum`, `exists_le_sum_fiber_of_sum_fiber_nonpos_of_nsmul_le_sum`, `exists_lt_card_fiber_of_mul_lt_card_of_maps_to`, `exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to`, `exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum`, `exists_lt_sum_fiber_of_sum_fiber_nonpos_of_nsmul_lt_sum`, `exists_sum_fiber_le_of_maps_to_of_sum_le_nsmul`, `exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul`, `exists_sum_fiber_lt_of_maps_to_of_sum_lt_nsmul`, `exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul`, `exists_card_fiber_le_of_card_le_mul`, `exists_card_fiber_le_of_card_le_nsmul`, `exists_card_fiber_lt_of_card_lt_mul`, `exists_card_fiber_lt_of_card_lt_nsmul`, `exists_le_card_fiber_of_mul_le_card`, `exists_le_card_fiber_of_nsmul_le_card`, `exists_le_sum_fiber_of_nsmul_le_sum`, `exists_lt_card_fiber_of_mul_lt_card`, `exists_lt_card_fiber_of_nsmul_lt_card`, `exists_lt_sum_fiber_of_nsmul_lt_sum`, `exists_sum_fiber_le_of_sum_le_nsmul`, `exists_sum_fiber_lt_of_sum_lt_nsmul`, `exists_lt_modEq_of_infinite`	29
Total	29

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_card_fiber_le_of_card_le_mul` 📖	mathematical	`Nonempty` `card`	`Finset` `instMembership` `filter`	—	`exists_card_fiber_le_of_card_le_nsmul` `Nat.instIsStrictOrderedRing`
`exists_card_fiber_le_of_card_le_nsmul` 📖	mathematical	`Nonempty` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `card` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid`	`Finset` `instMembership` `filter`	—	`cast_card` `exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `zero_le_one` `IsStrictOrderedRing.toZeroLEOneClass`
`exists_card_fiber_lt_of_card_lt_mul` 📖	mathematical	`card`	`Finset` `instMembership` `filter`	—	`exists_card_fiber_lt_of_card_lt_nsmul` `Nat.instIsStrictOrderedRing`
`exists_card_fiber_lt_of_card_lt_nsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `card` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid`	`Finset` `instMembership` `filter`	—	`cast_card` `exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `zero_le_one` `IsStrictOrderedRing.toZeroLEOneClass`
`exists_le_card_fiber_of_mul_le_card_of_maps_to` 📖	mathematical	`Finset` `instMembership` `Nonempty` `card`	`filter`	—	`exists_le_card_fiber_of_nsmul_le_card_of_maps_to` `Nat.instIsStrictOrderedRing`
`exists_le_card_fiber_of_nsmul_le_card_of_maps_to` 📖	mathematical	`Finset` `instMembership` `Nonempty` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `card` `AddMonoidWithOne.toNatCast`	`filter`	—	`cast_card` `exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid`
`exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum` 📖	mathematical	`Finset` `instMembership` `Nonempty` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `card` `sum`	`filter`	—	`exists_le_of_sum_le` `sum_const` `sum_fiberwise_of_maps_to`
`exists_le_sum_fiber_of_sum_fiber_nonpos_of_nsmul_le_sum` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `sum` `filter` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nonempty` `AddMonoid.toNatSMul` `card`	`Finset` `instMembership`	—	`exists_le_of_sum_le` `sum_const` `sum_le_sum_fiberwise_of_sum_fiber_nonpos` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid`
`exists_lt_card_fiber_of_mul_lt_card_of_maps_to` 📖	mathematical	`Finset` `instMembership` `card`	`filter`	—	`exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to` `Nat.instIsStrictOrderedRing`
`exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to` 📖	mathematical	`Finset` `instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `card` `AddMonoidWithOne.toNatCast`	`filter`	—	`cast_card` `exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid`
`exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum` 📖	mathematical	`Finset` `instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `card` `sum`	`filter`	—	`exists_lt_of_sum_lt` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `sum_const` `sum_fiberwise_of_maps_to`
`exists_lt_sum_fiber_of_sum_fiber_nonpos_of_nsmul_lt_sum` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `sum` `filter` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Preorder.toLT` `AddMonoid.toNatSMul` `card`	`Finset` `instMembership`	—	`exists_lt_of_sum_lt` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `sum_const` `sum_le_sum_fiberwise_of_sum_fiber_nonpos`
`exists_sum_fiber_le_of_maps_to_of_sum_le_nsmul` 📖	mathematical	`Finset` `instMembership` `Nonempty` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `sum` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `card`	`filter`	—	`exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum` `OrderDual.isOrderedAddCancelMonoid`
`exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `sum` `filter` `Nonempty` `AddMonoid.toNatSMul` `card`	`Finset` `instMembership`	—	`exists_le_sum_fiber_of_sum_fiber_nonpos_of_nsmul_le_sum` `OrderDual.isOrderedAddCancelMonoid`
`exists_sum_fiber_lt_of_maps_to_of_sum_lt_nsmul` 📖	mathematical	`Finset` `instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `sum` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `card`	`filter`	—	`exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum` `OrderDual.isOrderedAddCancelMonoid`
`exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `sum` `filter` `Preorder.toLT` `AddMonoid.toNatSMul` `card`	`Finset` `instMembership`	—	`exists_lt_sum_fiber_of_sum_fiber_nonpos_of_nsmul_lt_sum` `OrderDual.isOrderedAddCancelMonoid`

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_card_fiber_le_of_card_le_mul` 📖	mathematical	`card`	`Finset.card` `Finset.filter` `Finset.univ`	—	`exists_card_fiber_le_of_card_le_nsmul` `Nat.instIsStrictOrderedRing`
`exists_card_fiber_le_of_card_le_nsmul` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `card` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid`	`Finset.card` `Finset.filter` `Finset.univ`	—	`Finset.exists_card_fiber_le_of_card_le_nsmul` `Finset.univ_nonempty`
`exists_card_fiber_lt_of_card_lt_mul` 📖	mathematical	`card`	`Finset.card` `Finset.filter` `Finset.univ`	—	`exists_card_fiber_lt_of_card_lt_nsmul` `Nat.instIsStrictOrderedRing`
`exists_card_fiber_lt_of_card_lt_nsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `card` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid`	`Finset.card` `Finset.filter` `Finset.univ`	—	`Finset.exists_card_fiber_lt_of_card_lt_nsmul`
`exists_le_card_fiber_of_mul_le_card` 📖	mathematical	`card`	`Finset.card` `Finset.filter` `Finset.univ`	—	`exists_le_card_fiber_of_nsmul_le_card` `Nat.instIsStrictOrderedRing`
`exists_le_card_fiber_of_nsmul_le_card` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `card` `AddMonoidWithOne.toNatCast`	`Finset.card` `Finset.filter` `Finset.univ`	—	`Finset.exists_le_card_fiber_of_nsmul_le_card_of_maps_to` `Finset.mem_univ` `Finset.univ_nonempty`
`exists_le_sum_fiber_of_nsmul_le_sum` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `card` `Finset.sum` `Finset.univ`	`Finset.filter`	—	`Finset.exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum` `Finset.mem_univ` `Finset.univ_nonempty`
`exists_lt_card_fiber_of_mul_lt_card` 📖	mathematical	`card`	`Finset.card` `Finset.filter` `Finset.univ`	—	`exists_lt_card_fiber_of_nsmul_lt_card` `Nat.instIsStrictOrderedRing`
`exists_lt_card_fiber_of_nsmul_lt_card` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `card` `AddMonoidWithOne.toNatCast`	`Finset.card` `Finset.filter` `Finset.univ`	—	`Finset.exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to` `Finset.mem_univ`
`exists_lt_sum_fiber_of_nsmul_lt_sum` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `card` `Finset.sum` `Finset.univ`	`Finset.filter`	—	`Finset.exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum` `Finset.mem_univ`
`exists_sum_fiber_le_of_sum_le_nsmul` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Finset.sum` `Finset.univ` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `card`	`Finset.filter`	—	`exists_le_sum_fiber_of_nsmul_le_sum` `OrderDual.isOrderedAddCancelMonoid`
`exists_sum_fiber_lt_of_sum_lt_nsmul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Finset.sum` `Finset.univ` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `card`	`Finset.filter`	—	`exists_lt_sum_fiber_of_nsmul_lt_sum` `OrderDual.isOrderedAddCancelMonoid`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_lt_modEq_of_infinite` 📖	mathematical	`Set.Infinite`	`Set` `Set.instMembership` `ModEq`	—	`Set.Infinite.exists_lt_map_eq_of_mapsTo` `Set.finite_lt_nat`

---

← Back to Index