Documentation Verification Report

HarrisKleitman

📁 Source: Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean

Statistics

Metric	Count
Definitions	0
Theorems `card_inter_le_finset`, `le_card_inter_finset`, `le_card_inter_finset'`, `memberSubfamily`, `memberSubfamily_subset_nonMemberSubfamily`, `nonMemberSubfamily`, `card_inter_le_finset`, `le_card_inter_finset`	8
Total	8

IsLowerSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_inter_le_finset` 📖	mathematical	`IsLowerSet` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.partialOrder` `SetLike.coe` `Finset.instSetLike` `IsUpperSet`	`Monoid.toNatPow` `Nat.instMonoid` `Fintype.card` `Finset.card` `Finset.instInter` `Finset.decidableEq`	—	`Finset.inter_comm` `mul_comm` `IsUpperSet.card_inter_le_finset`
`le_card_inter_finset` 📖	mathematical	`IsLowerSet` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.partialOrder` `SetLike.coe` `Finset.instSetLike`	`Finset.card` `Monoid.toNatPow` `Nat.instMonoid` `Fintype.card` `Finset.instInter` `Finset.decidableEq`	—	`le_card_inter_finset'` `Finset.subset_univ`
`le_card_inter_finset'` 📖	mathematical	`IsLowerSet` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.partialOrder` `SetLike.coe` `Finset.instSetLike` `Finset.instHasSubset`	`Finset.card` `Monoid.toNatPow` `Nat.instMonoid` `Finset.instInter` `Finset.decidableEq`	—	`Finset.induction` `MulZeroClass.zero_mul` `Finset.empty_inter` `MulZeroClass.mul_zero` `Finset.inter_empty` `Finset.card_singleton` `pow_zero` `Finset.inter_singleton_of_mem` `Finset.card_insert_of_notMem` `Finset.card_memberSubfamily_add_card_nonMemberSubfamily` `add_mul` `Distrib.rightDistribClass` `mul_add` `Distrib.leftDistribClass` `add_comm` `add_add_add_comm` `le_imp_le_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `mul_add_mul_le_mul_add_mul` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedRing.toMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Finset.card_le_card` `memberSubfamily_subset_nonMemberSubfamily` `le_refl` `Nat.instAtLeastTwoHAddOfNat` `two_mul` `pow_succ'` `mul_assoc` `Finset.subset_insert_iff_of_notMem` `Finset.mem_nonMemberSubfamily` `Finset.mem_memberSubfamily` `HasSubset.Subset.trans` `Finset.instIsTransSubset` `Finset.subset_insert` `mul_le_mul_right` `Nat.instMulLeftMono` `LE.le.trans_eq` `add_le_add` `memberSubfamily` `nonMemberSubfamily` `Finset.memberSubfamily_inter` `Finset.nonMemberSubfamily_inter`
`memberSubfamily` 📖	mathematical	`IsLowerSet` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.partialOrder` `SetLike.coe` `Finset.instSetLike`	`Finset.memberSubfamily`	—	`Finset.insert_subset_insert`
`memberSubfamily_subset_nonMemberSubfamily` 📖	mathematical	`IsLowerSet` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.partialOrder` `SetLike.coe` `Finset.instSetLike`	`Finset.instHasSubset` `Finset.memberSubfamily` `Finset.nonMemberSubfamily`	—	`Finset.mem_memberSubfamily` `Finset.mem_nonMemberSubfamily` `Finset.subset_insert`
`nonMemberSubfamily` 📖	mathematical	`IsLowerSet` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.partialOrder` `SetLike.coe` `Finset.instSetLike`	`Finset.nonMemberSubfamily`	—	—

IsUpperSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_inter_le_finset` 📖	mathematical	`IsUpperSet` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.partialOrder` `SetLike.coe` `Finset.instSetLike` `IsLowerSet`	`Monoid.toNatPow` `Nat.instMonoid` `Fintype.card` `Finset.card` `Finset.instInter` `Finset.decidableEq`	—	`IsLowerSet.le_card_inter_finset` `Finset.coe_compl` `isLowerSet_compl` `inf_comm` `sdiff_compl` `Finset.sdiff_inter_self_right` `Finset.card_sdiff_of_subset` `Finset.inter_subset_right` `mul_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `LE.total` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `tsub_le_iff_tsub_le` `tsub_mul` `covariant_swap_mul_of_covariant_mul` `Nat.instMulLeftMono` `Fintype.card_finset` `Finset.card_compl`
`le_card_inter_finset` 📖	mathematical	`IsUpperSet` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.partialOrder` `SetLike.coe` `Finset.instSetLike`	`Finset.card` `Monoid.toNatPow` `Nat.instMonoid` `Fintype.card` `Finset.instInter` `Finset.decidableEq`	—	`IsLowerSet.card_inter_le_finset` `Finset.coe_compl` `isLowerSet_compl` `inf_comm` `sdiff_compl` `Finset.sdiff_inter_self_right` `Finset.card_sdiff_of_subset` `Finset.inter_subset_right` `mul_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `LE.total` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `le_tsub_iff_le_tsub` `CanonicallyOrderedAdd.toExistsAddOfLE` `le_imp_le_of_le_of_le` `mul_le_mul_right` `Nat.instMulLeftMono` `Finset.card_le_card` `le_refl` `Fintype.card_finset` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `Finset.card_le_univ` `tsub_mul` `Finset.card_compl`

---

← Back to Index