Kleitman

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

Statistics

Metric	Count
Definitions	0
Theorems card_biUnion_le_of_intersecting	1
Total	1

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_biUnion_le_of_intersecting 📖	mathematical	Set.Intersecting Finset Lattice.toSemilatticeInf instLattice instOrderBot SetLike.coe instSetLike	card biUnion decidableEq Monoid.toNatPow Nat.instMonoid Fintype.card	—	le_total tsub_eq_zero_of_le Nat.instCanonicallyOrderedAdd Nat.instOrderedSub pow_zero LE.le.trans_eq card_le_card biUnion_subset mem_compl notMem_singleton Set.Intersecting.ne_bot card_compl Fintype.card_finset card_singleton cons_induction tsub_zero tsub_self Set.Intersecting.exists_card_eq instNontrivial Set.Intersecting.isUpperSet' Set.Intersecting.is_max_iff_card_eq LE.le.trans biUnion_mono cons_eq_insert biUnion_insert card_mono le_sup_sdiff card_union_le union_sdiff_left sdiff_eq_inter_compl le_of_mul_le_mul_left Nat.instAtLeastTwoHAddOfNat PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono pow_succ mul_add Distrib.leftDistribClass mul_assoc mul_comm add_le_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add mul_le_mul_iff_right₀ IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing pow_pos Nat.instZeroLEOneClass zero_lt_two' Set.Intersecting.card_le mem_cons_self IsUpperSet.card_inter_le_finset coe_biUnion isUpperSet_iUnion₂ subset_cons coe_compl IsUpperSet.compl mul_tsub LE.total IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le mul_left_comm two_mul add_tsub_cancel_left mul_two add_mul Distrib.rightDistribClass mul_le_mul_right Nat.instMulLeftMono add_le_add_right pow_succ' add_tsub_assoc_of_le CanonicallyOrderedAdd.toExistsAddOfLE pow_right_mono₀ one_le_two tsub_le_self tsub_add_eq_add_tsub card_cons add_tsub_add_eq_tsub_right le_refl

---

← Back to Index