DoubleCounting

📁 Source: Mathlib/Combinatorics/Enumerative/DoubleCounting.lean

Statistics

Metric	Count
Definitions `bipartiteAbove`, `bipartiteBelow`	2
Theorems `bipartiteAbove_swap`, `bipartiteBelow_swap`, `card_le_card_of_forall_subsingleton`, `card_le_card_of_forall_subsingleton'`, `card_mul_eq_card_mul`, `card_mul_le_card_mul`, `card_mul_le_card_mul'`, `card_nsmul_le_card_nsmul`, `card_nsmul_le_card_nsmul'`, `card_nsmul_lt_card_nsmul_of_le_of_lt`, `card_nsmul_lt_card_nsmul_of_le_of_lt'`, `card_nsmul_lt_card_nsmul_of_lt_of_le`, `card_nsmul_lt_card_nsmul_of_lt_of_le'`, `coe_bipartiteAbove`, `coe_bipartiteBelow`, `mem_bipartiteAbove`, `mem_bipartiteBelow`, `prod_prod_bipartiteAbove_eq_prod_prod_bipartiteBelow`, `sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow`, `sum_sum_bipartiteAbove_eq_sum_sum_bipartiteBelow`, `card_le_card_of_leftTotal_unique`, `card_le_card_of_rightTotal_unique`	22
Total	24

Finset

Definitions

Name	Category	Theorems
`bipartiteAbove` 📖	CompOp	8 math math: `sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow`, `coe_bipartiteAbove`, `sum_sum_bipartiteAbove_eq_sum_sum_bipartiteBelow`, `bipartiteBelow_swap`, `bipartiteAbove_swap`, `mem_bipartiteAbove`, `SimpleGraph.isBipartiteWith_bipartiteAbove`, `prod_prod_bipartiteAbove_eq_prod_prod_bipartiteBelow`
`bipartiteBelow` 📖	CompOp	8 math math: `sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow`, `coe_bipartiteBelow`, `sum_sum_bipartiteAbove_eq_sum_sum_bipartiteBelow`, `SimpleGraph.isBipartiteWith_bipartiteBelow`, `bipartiteBelow_swap`, `mem_bipartiteBelow`, `bipartiteAbove_swap`, `prod_prod_bipartiteAbove_eq_prod_prod_bipartiteBelow`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bipartiteAbove_swap` 📖	mathematical	—	`bipartiteAbove` `Function.swap` `bipartiteBelow`	—	—
`bipartiteBelow_swap` 📖	mathematical	—	`bipartiteBelow` `Function.swap` `bipartiteAbove`	—	—
`card_le_card_of_forall_subsingleton` 📖	mathematical	`Finset` `instMembership` `Set.Subsingleton` `setOf`	`card`	—	`mul_one` `card_mul_le_card_mul` `card_pos` `coe_nonempty` `coe_bipartiteAbove` `card_le_one`
`card_le_card_of_forall_subsingleton'` 📖	mathematical	`Finset` `instMembership` `Set.Subsingleton` `setOf`	`card`	—	`card_le_card_of_forall_subsingleton`
`card_mul_eq_card_mul` 📖	—	`card` `bipartiteAbove` `bipartiteBelow`	—	—	`LE.le.antisymm` `card_mul_le_card_mul` `Eq.ge` `Eq.le` `card_mul_le_card_mul'`
`card_mul_le_card_mul` 📖	—	`card` `bipartiteAbove` `bipartiteBelow`	—	—	`card_nsmul_le_card_nsmul` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing`
`card_mul_le_card_mul'` 📖	—	`card` `bipartiteBelow` `bipartiteAbove`	—	—	`card_nsmul_le_card_nsmul'` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing`
`card_nsmul_le_card_nsmul` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `card` `bipartiteAbove` `bipartiteBelow`	`AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid`	—	`card_nsmul_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow` `sum_le_card_nsmul`
`card_nsmul_le_card_nsmul'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `card` `bipartiteBelow` `bipartiteAbove`	`AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid`	—	`card_nsmul_le_card_nsmul`
`card_nsmul_lt_card_nsmul_of_le_of_lt` 📖	mathematical	`Nonempty` `Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `card` `bipartiteAbove` `Preorder.toLT` `bipartiteBelow`	`AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid`	—	`card_nsmul_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toCharZero` `sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow` `sum_lt_sum_of_nonempty` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `sum_const`
`card_nsmul_lt_card_nsmul_of_le_of_lt'` 📖	mathematical	`Nonempty` `Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `card` `bipartiteBelow` `Preorder.toLT` `bipartiteAbove`	`AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid`	—	`card_nsmul_lt_card_nsmul_of_le_of_lt`
`card_nsmul_lt_card_nsmul_of_lt_of_le` 📖	mathematical	`Nonempty` `Preorder.toLT` `PartialOrder.toPreorder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `card` `bipartiteAbove` `Preorder.toLE` `bipartiteBelow`	`AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid`	—	`sum_const` `sum_lt_sum_of_nonempty` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsStrictOrderedRing.toCharZero` `sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow` `sum_le_card_nsmul` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing`
`card_nsmul_lt_card_nsmul_of_lt_of_le'` 📖	mathematical	`Nonempty` `Preorder.toLT` `PartialOrder.toPreorder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `card` `bipartiteBelow` `Preorder.toLE` `bipartiteAbove`	`AddMonoid.toNatSMul` `AddMonoidWithOne.toAddMonoid`	—	`card_nsmul_lt_card_nsmul_of_lt_of_le`
`coe_bipartiteAbove` 📖	mathematical	—	`SetLike.coe` `Finset` `instSetLike` `bipartiteAbove` `setOf` `instMembership`	—	`coe_filter`
`coe_bipartiteBelow` 📖	mathematical	—	`SetLike.coe` `Finset` `instSetLike` `bipartiteBelow` `setOf` `instMembership`	—	`coe_filter`
`mem_bipartiteAbove` 📖	mathematical	—	`Finset` `instMembership` `bipartiteAbove`	—	`mem_filter`
`mem_bipartiteBelow` 📖	mathematical	—	`Finset` `instMembership` `bipartiteBelow`	—	`mem_filter`
`prod_prod_bipartiteAbove_eq_prod_prod_bipartiteBelow` 📖	mathematical	—	`prod` `bipartiteAbove` `bipartiteBelow`	—	`prod_congr` `prod_filter` `prod_comm`
`sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow` 📖	mathematical	—	`sum` `Nat.instAddCommMonoid` `card` `bipartiteAbove` `bipartiteBelow`	—	`sum_congr` `card_eq_sum_ones` `sum_sum_bipartiteAbove_eq_sum_sum_bipartiteBelow`
`sum_sum_bipartiteAbove_eq_sum_sum_bipartiteBelow` 📖	mathematical	—	`sum` `bipartiteAbove` `bipartiteBelow`	—	`sum_congr` `sum_filter` `sum_comm`

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_card_of_leftTotal_unique` 📖	mathematical	`Relator.LeftTotal` `Relator.LeftUnique`	`card`	—	`Finset.card_le_card_of_forall_subsingleton`
`card_le_card_of_rightTotal_unique` 📖	mathematical	`Relator.RightTotal` `Relator.RightUnique`	`card`	—	`Finset.card_le_card_of_forall_subsingleton'`

---

← Back to Index