Documentation Verification Report

LYM

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

Statistics

Metric	Count
Definitions `falling`	1
Theorems `disjoint_slice_shadow_falling`, `card_div_choose_le_card_shadow_div_choose`, `card_mul_le_card_shadow_mul`, `falling_zero_subset`, `le_card_falling_div_choose`, `local_lubell_yamamoto_meshalkin_inequality_div`, `local_lubell_yamamoto_meshalkin_inequality_mul`, `lubell_yamamoto_meshalkin_inequality_sum_card_div_choose`, `lubell_yamamoto_meshalkin_inequality_sum_inv_choose`, `mem_falling`, `sized_falling`, `slice_subset_falling`, `slice_union_shadow_falling_succ`, `sum_card_slice_div_choose_le_one`, `sperner`	15
Total	16

Finset

Definitions

Name	Category	Theorems
`falling` 📖	CompOp	7 math math: `falling_zero_subset`, `slice_subset_falling`, `le_card_falling_div_choose`, `slice_union_shadow_falling_succ`, `mem_falling`, `sized_falling`, `IsAntichain.disjoint_slice_shadow_falling`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_div_choose_le_card_shadow_div_choose` 📖	mathematical	`Set.Sized` `SetLike.coe` `Finset` `instSetLike`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `card` `Nat.choose` `Fintype.card` `shadow`	—	`local_lubell_yamamoto_meshalkin_inequality_div`
`card_mul_le_card_shadow_mul` 📖	mathematical	`Set.Sized` `SetLike.coe` `Finset` `instSetLike`	`card` `shadow` `Fintype.card`	—	`local_lubell_yamamoto_meshalkin_inequality_mul`
`falling_zero_subset` 📖	mathematical	—	`Finset` `instHasSubset` `falling` `instSingleton` `instEmptyCollection`	—	`subset_singleton_iff'` `card_eq_zero` `sized_falling`
`le_card_falling_div_choose` 📖	mathematical	`Fintype.card` `IsAntichain` `Finset` `instHasSubset` `SetLike.coe` `instSetLike`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `range` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `card` `slice` `Nat.choose` `falling`	—	`sum_congr` `zero_add` `sum_singleton` `tsub_zero` `Nat.instOrderedSub` `Nat.choose_self` `Nat.cast_one` `div_one` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `card_le_card` `slice_subset_falling` `sum_range_succ` `slice_union_shadow_falling_succ` `card_union_of_disjoint` `IsAntichain.disjoint_slice_shadow_falling` `Nat.cast_add` `add_div` `add_comm` `tsub_tsub` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `Nat.instIsOrderedAddMonoid` `le_tsub_of_add_le_left` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `le_imp_le_of_le_of_le` `add_le_add_right` `le_refl` `local_lubell_yamamoto_meshalkin_inequality_div` `LT.lt.ne'` `tsub_pos_iff_lt` `sized_falling`
`local_lubell_yamamoto_meshalkin_inequality_div` 📖	mathematical	`Set.Sized` `SetLike.coe` `Finset` `instSetLike`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `card` `Nat.choose` `Fintype.card` `shadow`	—	`lt_or_ge` `Nat.choose_eq_zero_of_lt` `Nat.cast_zero` `div_zero` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Nat.cast_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `local_lubell_yamamoto_meshalkin_inequality_mul` `div_le_div_iff₀` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Nat.choose_pos` `LE.le.trans` `le_of_mul_le_mul_right` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Nat.instIsStrictOrderedRing` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Nat.instIsOrderedAddMonoid` `mul_assoc` `IsCancelMulZero.toIsLeftCancelMulZero` `Nat.instIsCancelMulZero` `mul_comm` `Nat.choose_succ_right_eq` `add_tsub_add_eq_tsub_right` `tsub_add_eq_add_tsub` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `pos_iff_ne_zero`
`local_lubell_yamamoto_meshalkin_inequality_mul` 📖	mathematical	`Set.Sized` `SetLike.coe` `Finset` `instSetLike`	`card` `shadow` `Fintype.card`	—	`card_mul_le_card_mul'` `card_image_of_injOn` `erase_injOn` `card_le_card` `erase_mem_shadow` `erase_subset` `le_trans` `Set.Sized.shadow` `card_compl` `insert_inj_on'` `mem_coe` `Set.Sized.empty_mem_iff` `coe_eq_singleton` `notMem_empty` `shadow_singleton_empty` `mem_bipartiteAbove` `exists_eq_insert_iff` `sized_shadow_iff` `mem_image_of_mem` `mem_compl` `tsub_tsub_le_tsub_add` `Nat.instOrderedSub` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`lubell_yamamoto_meshalkin_inequality_sum_card_div_choose` 📖	mathematical	`IsAntichain` `Finset` `instHasSubset` `SetLike.coe` `instSetLike`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `range` `Fintype.card` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `card` `slice` `Nat.choose` `AddMonoidWithOne.toOne`	—	`sum_flip` `LE.le.trans` `le_card_falling_div_choose` `le_rfl` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Nat.cast_zero` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `Nat.choose_zero_right` `zero_lt_one` `Nat.instZeroLEOneClass` `Nat.cast_one` `one_mul` `Set.Sized.card_le` `sized_falling`
`lubell_yamamoto_meshalkin_inequality_sum_inv_choose` 📖	mathematical	`IsAntichain` `Finset` `instHasSubset` `SetLike.coe` `instSetLike`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.choose` `Fintype.card` `card` `AddMonoidWithOne.toOne`	—	`sum_fiberwise_of_maps_to'` `Nat.instNoMaxOrder` `sum_congr` `sum_const` `nsmul_eq_mul` `div_eq_mul_inv` `lubell_yamamoto_meshalkin_inequality_sum_card_div_choose`
`mem_falling` 📖	mathematical	—	`Finset` `instMembership` `falling` `instHasSubset` `card`	—	—
`sized_falling` 📖	mathematical	—	`Set.Sized` `SetLike.coe` `Finset` `instSetLike` `falling`	—	`mem_falling`
`slice_subset_falling` 📖	mathematical	—	`Finset` `instHasSubset` `slice` `falling`	—	`mem_falling` `Subset.refl` `mem_slice`
`slice_union_shadow_falling_succ` 📖	mathematical	—	`Finset` `instUnion` `decidableEq` `slice` `shadow` `falling`	—	`ext` `Subset.refl` `HasSubset.Subset.trans` `instIsTransSubset` `erase_subset` `card_erase_of_mem` `ssubset_iff` `ssubset_of_subset_of_ne` `instIsNonstrictStrictOrderSubsetSSubset` `instAntisymmSubset` `Membership.mem.ne_of_notMem` `card_insert_of_notMem` `mem_insert_self` `erase_insert`
`sum_card_slice_div_choose_le_one` 📖	mathematical	`IsAntichain` `Finset` `instHasSubset` `SetLike.coe` `instSetLike`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `range` `Fintype.card` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `card` `slice` `Nat.choose` `AddMonoidWithOne.toOne`	—	`lubell_yamamoto_meshalkin_inequality_sum_card_div_choose`

Finset.IsAntichain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_slice_shadow_falling` 📖	mathematical	`IsAntichain` `Finset` `Finset.instHasSubset` `SetLike.coe` `Finset.instSetLike`	`Disjoint` `Finset.partialOrder` `Finset.instOrderBot` `Finset.slice` `Finset.shadow` `Finset.falling`	—	`Finset.disjoint_right` `Finset.slice_subset` `Finset.notMem_erase` `HasSubset.Subset.trans` `Finset.instIsTransSubset` `Finset.erase_subset`

IsAntichain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sperner` 📖	mathematical	`IsAntichain` `Finset` `Finset.instHasSubset` `SetLike.coe` `Finset.instSetLike`	`Finset.card` `Nat.choose` `Fintype.card`	—	`Nat.cast_pos` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRingNNRat` `NNRat.instNontrivial` `Nat.choose_pos` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `inv_anti₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Nat.cast_zero` `IsStrictOrderedRing.toZeroLEOneClass` `NNRat.instCharZero` `Finset.card_le_univ` `Nat.mono_cast` `Nat.choose_le_middle` `Finset.lubell_yamamoto_meshalkin_inequality_sum_inv_choose` `Finset.sum_const` `nsmul_eq_mul` `mul_inv_le_iff₀'` `mul_one`

---

← Back to Index