Documentation Verification Report

KruskalKatona

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

Statistics

Metric	Count
Definitions	0
Theorems `shadow`, `shadow_initSeg`, `isInitSeg_of_compressed`, `toColex_compress_lt_toColex`, `erdos_ko_rado`, `iterated_kk`, `kruskal_katona`, `kruskal_katona_lovasz_form`	8
Total	8

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`erdos_ko_rado` 📖	mathematical	`Set.Intersecting` `Finset` `Lattice.toSemilatticeInf` `instLattice` `instOrderBot` `SetLike.coe` `instSetLike` `Set.Sized`	`card` `Nat.choose`	—	`card_eq_zero` `eq_empty_iff_forall_notMem` `disjoint_self_iff_empty` `le_of_not_gt` `disjoint_right` `disjoint_of_subset_left` `disjoint_compl_right` `LE.le.trans` `card_compls` `Nat.choose_symm_of_eq_add` `tsub_add_tsub_cancel` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `coe_compls` `Fintype.card_fin` `Set.Sized.compls` `kruskal_katona_lovasz_form` `tsub_le_tsub_iff_left` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `tsub_le_self` `LT.lt.le` `Nat.choose_succ_succ` `add_lt_add_of_lt_of_le` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `card_union_of_disjoint` `LT.lt.not_ge` `Set.Sized.card_le` `coe_union` `Set.sized_union` `Set.Sized.shadow_iterate`
`iterated_kk` 📖	mathematical	`Set.Sized` `SetLike.coe` `Finset` `instSetLike` `card` `Colex.IsInitSeg` `Fin.instLinearOrder`	`Nat.iterate` `shadow`	—	`Set.Sized.shadow` `kruskal_katona` `Colex.IsInitSeg.shadow` `Finite.of_fintype`
`kruskal_katona` 📖	mathematical	`Set.Sized` `SetLike.coe` `Finset` `instSetLike` `card` `Colex.IsInitSeg` `Fin.instLinearOrder`	`shadow`	—	`exists_subset_card_eq` `Set.Sized.mono` `Colex.IsInitSeg.total` `UV.isInitSeg_of_compressed` `eq_of_subset_of_card_le` `Eq.le` `Eq.ge` `LE.le.trans` `card_le_card` `shadow_mono`
`kruskal_katona_lovasz_form` 📖	mathematical	`Set.Sized` `SetLike.coe` `Finset` `instSetLike` `Nat.choose` `card`	`Nat.iterate` `shadow`	—	`mem_range` `forall_lt_iff_le` `Set.sized_powersetCard` `card_powersetCard` `card_attachFin` `card_range` `ext` `mem_powersetCard` `mem_shadow_iterate_iff_exists_sdiff` `exists_subsuperset_card_eq` `card_sdiff_of_subset` `HasSubset.Subset.trans` `instIsTransSubset` `eq_tsub_of_add_eq` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `add_comm` `card_sdiff_add_card_eq_card` `iterated_kk` `mem_attachFin` `Colex.toColex_image_lt_toColex_image` `Fin.val_strictMono` `Colex.forall_lt_mono` `LT.lt.le` `mem_image`

Finset.Colex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`shadow_initSeg` 📖	mathematical	`Finset.Nonempty`	`Finset.shadow` `LinearOrder.toDecidableEq` `initSeg` `Finset.erase` `Finset.min'`	—	`Finset.ext` `Finset.card_erase_of_mem` `Finset.min'_mem` `Finset.card_insert_of_notMem` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Finset.card_pos` `LT.lt.trans_le` `Finset.mem_insert_self` `Eq.ge` `Finset.erase_insert_eq_erase` `Finset.erase_eq_of_notMem` `erase_le_erase_min'` `Finset.notMem_erase` `Finset.insert_erase` `Finset.mem_compl` `Finset.min'_le` `Finset.card_erase_add_one` `LE.le.lt_or_eq` `Finset.mem_of_mem_erase` `Finset.mem_of_mem_insert_of_ne` `LT.lt.ne'` `LT.lt.trans` `LE.le.trans_lt` `Finset.eq_of_subset_of_card_le` `lt_trichotomy` `Finset.mem_insert_of_mem` `Finset.mem_erase_of_ne_of_mem` `lt_of_le_of_lt` `LE.le.not_gt`

Finset.Colex.IsInitSeg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`shadow` 📖	mathematical	`Finset.Colex.IsInitSeg`	`Finset.shadow` `LinearOrder.toDecidableEq`	—	`nonempty_fintype` `Finset.mem_singleton` `Finset.card_eq_zero` `Finset.shadow_monotone` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `Finset.eq_empty_or_nonempty` `exists_initSeg` `Finset.card_pos` `Finset.Colex.shadow_initSeg` `Finset.card_erase_of_mem` `Finset.min'_mem` `Finset.Colex.isInitSeg_initSeg`

Finset.UV

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isInitSeg_of_compressed` 📖	mathematical	`Set.Sized` `SetLike.coe` `Finset` `Finset.instSetLike` `UV.IsCompressed` `Finset.instGeneralizedBooleanAlgebra` `LinearOrder.toDecidableEq` `Finset.decidableDisjoint` `Finset.instDecidableLE` `Finset.decidableEq`	`Finset.Colex.IsInitSeg`	—	`Finset.sdiff_nonempty` `Finset.eq_of_subset_of_card_le` `Eq.ge` `Eq.le` `Disjoint.mono_left` `Finset.sdiff_subset` `Finset.disjoint_sdiff` `lt_trichotomy` `LT.lt.not_gt` `UV.compress_sdiff_sdiff` `toColex_compress_lt_toColex` `Finset.disjoint_right` `Finset.max'_mem` `UV.IsCompressed.eq` `Finset.card_sdiff_comm` `UV.mem_compression`
`toColex_compress_lt_toColex` 📖	mathematical	`Finset.Nonempty` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Finset.max'`	`Colex` `Finset` `Finset.Colex.instPartialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `UV.compress` `Finset.instGeneralizedBooleanAlgebra` `LinearOrder.toDecidableEq` `Finset.decidableDisjoint` `Finset.instDecidableLE`	—	`UV.compress.eq_1` `ite_ne_right_iff` `Finset.Colex.lt_iff_exists_filter_lt` `Finset.mem_sdiff` `Finset.max'_mem` `Finset.notMem_sdiff_of_mem_right` `LT.lt.not_ge` `Finset.le_max'` `LT.lt.not_gt` `LE.le.trans_lt`

---

← Back to Index