Documentation Verification Report

InclusionExclusion

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

Statistics

Metric	Count
Definitions	0
Theorems `inclusion_exclusion_card_biUnion`, `inclusion_exclusion_card_inf_compl`, `inclusion_exclusion_sum_biUnion`, `inclusion_exclusion_sum_inf_compl`, `indicator_biUnion_eq_sum_powerset`, `prod_indicator_biUnion_finset_sub_indicator`, `prod_indicator_biUnion_sub_indicator`	7
Total	7

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inclusion_exclusion_card_biUnion` 📖	mathematical	—	`card` `biUnion` `sum` `Finset` `SetLike.instMembership` `instSetLike` `filter` `Nonempty` `decidableNonempty` `powerset` `Int.instAddCommMonoid` `univ` `Subtype.fintype` `Monoid.toNatPow` `Int.instMonoid` `inf'` `Lattice.toSemilatticeInf` `instLattice` `instMembership` `mem_filter`	—	`mem_filter` `sum_congr` `sum_const` `mul_one` `inclusion_exclusion_sum_biUnion`
`inclusion_exclusion_card_inf_compl` 📖	mathematical	—	`card` `inf` `Finset` `Lattice.toSemilatticeInf` `instLattice` `CoheytingAlgebra.toOrderTop` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `booleanAlgebra` `Compl.compl` `BooleanAlgebra.toCompl` `sum` `Int.instAddCommMonoid` `powerset` `Monoid.toNatPow` `Int.instMonoid`	—	`sum_congr` `sum_const` `mul_one` `inclusion_exclusion_sum_inf_compl`
`inclusion_exclusion_sum_biUnion` 📖	mathematical	—	`sum` `AddCommGroup.toAddCommMonoid` `biUnion` `Finset` `SetLike.instMembership` `instSetLike` `filter` `Nonempty` `decidableNonempty` `powerset` `univ` `Subtype.fintype` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Monoid.toNatPow` `Int.instMonoid` `card` `inf'` `Lattice.toSemilatticeInf` `instLattice` `instMembership` `mem_filter`	—	`mem_filter` `sub_eq_zero` `sum_congr` `pow_succ` `mul_neg` `mul_one` `neg_smul` `sub_eq_neg_add` `neg_neg` `filter.congr_simp` `filter_eq'` `sum_singleton` `pow_zero` `one_smul` `sum_attach` `smul_dite` `sum_dite` `prod_sub` `mul_assoc` `sum_smul` `sum_comm` `prod_const_one` `prod_indicator_apply` `smul_sum` `mul_ite` `MulZeroClass.mul_zero` `ite_smul` `zero_smul` `sum_ite` `sum_const_zero` `add_zero` `ext` `prod_congr` `sdiff_empty` `not_nonempty_iff_eq_empty` `Set.indicator_of_mem` `Pi.one_apply` `eq_empty_or_nonempty` `coe_empty` `Set.indicator_of_notMem` `zero_sub` `prod_indicator_biUnion_finset_sub_indicator`
`inclusion_exclusion_sum_inf_compl` 📖	mathematical	—	`sum` `AddCommGroup.toAddCommMonoid` `inf` `Finset` `Lattice.toSemilatticeInf` `instLattice` `CoheytingAlgebra.toOrderTop` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `booleanAlgebra` `Compl.compl` `BooleanAlgebra.toCompl` `powerset` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Monoid.toNatPow` `Int.instMonoid` `card`	—	`compl_sup` `sup_eq_biUnion` `eq_sub_iff_add_eq` `sum_compl_add_sum` `mem_filter` `inclusion_exclusion_sum_biUnion` `sum_congr` `pow_succ` `mul_neg` `mul_one` `inf'_eq_inf` `neg_smul` `sum_neg_distrib` `sub_eq_add_neg` `neg_neg` `filter.congr_simp` `filter_eq'` `sum_singleton` `pow_zero` `one_smul` `sum_attach` `sum_filter_not_add_sum_filter`
`indicator_biUnion_eq_sum_powerset` 📖	mathematical	—	`Set.indicator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set.iUnion` `Finset` `instMembership` `sum` `AddCommGroup.toAddCommMonoid` `filter` `Nonempty` `decidableNonempty` `powerset` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Monoid.toNatPow` `Int.instMonoid` `card` `Set.iInter`	—	`sub_eq_zero` `Set.indicator_of_mem` `sum_congr` `pow_succ` `mul_neg` `mul_one` `neg_smul` `sub_eq_neg_add` `neg_neg` `filter.congr_simp` `filter_eq'` `sum_singleton` `pow_zero` `Set.iInter_congr_Prop` `Set.iInter_of_empty` `instIsEmptyFalse` `Set.iInter_univ` `one_smul` `sum_filter_add_sum_filter_not` `prod_sub` `prod_const_one` `sum_smul` `prod_indicator_apply` `smul_ite` `smul_zero` `mul_ite` `MulZeroClass.mul_zero` `ite_smul` `zero_smul` `prod_indicator_biUnion_sub_indicator` `Set.indicator_of_notMem` `sum_eq_zero` `Mathlib.Tactic.Contrapose.contrapose₄`
`prod_indicator_biUnion_finset_sub_indicator` 📖	mathematical	`Nonempty`	`prod` `Int.instCommMonoid` `Set.indicator` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `SetLike.coe` `Finset` `instSetLike` `biUnion` `Pi.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing`	—	`prod_congr` `coe_biUnion` `Set.iUnion_congr_Prop` `prod_indicator_biUnion_sub_indicator`
`prod_indicator_biUnion_sub_indicator` 📖	mathematical	`Nonempty`	`prod` `Int.instCommMonoid` `Set.indicator` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `Set.iUnion` `Finset` `instMembership` `Pi.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing`	—	`prod_eq_zero` `Set.indicator_of_mem` `sub_self` `Set.indicator_of_notMem`

---

← Back to Index