Shadow

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

Statistics

Metric	Count
Definitions `shadow`, `upShadow`, `«term∂»`, `«term∂⁺»`	4
Theorems `erase_mem_shadow`, `exists_subset_of_mem_shadow`, `exists_subset_of_mem_upShadow`, `insert_mem_upShadow`, `mem_shadow_iff`, `mem_shadow_iff_exists_mem_card_add_one`, `mem_shadow_iff_exists_sdiff`, `mem_shadow_iff_insert_mem`, `mem_shadow_iterate_iff_exists_card`, `mem_shadow_iterate_iff_exists_mem_card_add`, `mem_shadow_iterate_iff_exists_sdiff`, `mem_upShadow_iff`, `mem_upShadow_iff_erase_mem`, `mem_upShadow_iff_exists_mem_card_add`, `mem_upShadow_iff_exists_mem_card_add_one`, `mem_upShadow_iff_exists_sdiff`, `mem_upShadow_iterate_iff_exists_card`, `mem_upShadow_iterate_iff_exists_mem_card_add`, `mem_upShadow_iterate_iff_exists_sdiff`, `shadow_compls`, `shadow_empty`, `shadow_iterate_empty`, `shadow_mono`, `shadow_monotone`, `shadow_singleton`, `shadow_singleton_empty`, `sized_shadow_iff`, `upShadow_compls`, `upShadow_empty`, `upShadow_monotone`, `shadow`, `shadow_iterate`, `upShadow`	33
Total	37

Finset

Definitions

Name	Category	Theorems
`shadow` 📖	CompOp	32 math math: `Set.Sized.shadow_iterate`, `UV.shadow_compression_subset_compression_shadow`, `mem_shadow_iterate_iff_exists_sdiff`, `local_lubell_yamamoto_meshalkin_inequality_mul`, `card_mul_le_card_shadow_mul`, `shadow_compls`, `card_div_choose_le_card_shadow_div_choose`, `local_lubell_yamamoto_meshalkin_inequality_div`, `UV.card_shadow_compression_le`, `iterated_kk`, `erase_mem_shadow`, `kruskal_katona`, `mem_shadow_iff_insert_mem`, `shadow_singleton`, `shadow_singleton_empty`, `slice_union_shadow_falling_succ`, `Colex.shadow_initSeg`, `shadow_empty`, `Colex.IsInitSeg.shadow`, `shadow_mono`, `mem_shadow_iterate_iff_exists_card`, `sized_shadow_iff`, `shadow_iterate_empty`, `mem_shadow_iff_exists_sdiff`, `shadow_monotone`, `upShadow_compls`, `mem_shadow_iff`, `mem_shadow_iterate_iff_exists_mem_card_add`, `mem_shadow_iff_exists_mem_card_add_one`, `Set.Sized.shadow`, `IsAntichain.disjoint_slice_shadow_falling`, `kruskal_katona_lovasz_form`
`upShadow` 📖	CompOp	14 math math: `mem_upShadow_iff_exists_mem_card_add`, `shadow_compls`, `Set.Sized.upShadow`, `upShadow_empty`, `mem_upShadow_iterate_iff_exists_card`, `upShadow_monotone`, `mem_upShadow_iff_exists_sdiff`, `upShadow_compls`, `mem_upShadow_iff_erase_mem`, `mem_upShadow_iff_exists_mem_card_add_one`, `mem_upShadow_iff`, `insert_mem_upShadow`, `mem_upShadow_iterate_iff_exists_sdiff`, `mem_upShadow_iterate_iff_exists_mem_card_add`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`erase_mem_shadow` 📖	mathematical	`Finset` `instMembership`	`shadow` `erase`	—	`mem_shadow_iff`
`exists_subset_of_mem_shadow` 📖	mathematical	`Finset` `instMembership` `shadow`	`instHasSubset`	—	`mem_shadow_iff_exists_mem_card_add_one`
`exists_subset_of_mem_upShadow` 📖	mathematical	`Finset` `instMembership` `upShadow`	`instHasSubset`	—	`mem_upShadow_iff_exists_mem_card_add_one`
`insert_mem_upShadow` 📖	mathematical	`Finset` `instMembership`	`upShadow` `instInsert`	—	`mem_upShadow_iff`
`mem_shadow_iff` 📖	mathematical	—	`Finset` `instMembership` `shadow` `erase`	—	—
`mem_shadow_iff_exists_mem_card_add_one` 📖	mathematical	—	`Finset` `instMembership` `shadow` `instHasSubset` `card`	—	`mem_shadow_iff_exists_sdiff` `card_sdiff_of_subset` `tsub_eq_iff_eq_add_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `card_mono` `add_comm`
`mem_shadow_iff_exists_sdiff` 📖	mathematical	—	`Finset` `instMembership` `shadow` `instHasSubset` `card` `instSDiff`	—	—
`mem_shadow_iff_insert_mem` 📖	mathematical	—	`Finset` `instMembership` `shadow` `instInsert`	—	—
`mem_shadow_iterate_iff_exists_card` 📖	mathematical	—	`Finset` `instMembership` `Nat.iterate` `shadow` `card` `Disjoint` `partialOrder` `instOrderBot` `instUnion`	—	`union_empty` `Function.iterate_succ_apply'` `insert_union` `union_insert`
`mem_shadow_iterate_iff_exists_mem_card_add` 📖	mathematical	—	`Finset` `instMembership` `Nat.iterate` `shadow` `instHasSubset` `card`	—	`mem_shadow_iterate_iff_exists_sdiff` `card_sdiff_of_subset` `tsub_eq_iff_eq_add_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `card_mono` `add_comm`
`mem_shadow_iterate_iff_exists_sdiff` 📖	mathematical	—	`Finset` `instMembership` `Nat.iterate` `shadow` `instHasSubset` `card` `instSDiff`	—	`mem_shadow_iterate_iff_exists_card` `subset_union_left` `union_sdiff_cancel_left` `disjoint_sdiff` `union_sdiff_self_eq_union` `union_eq_right`
`mem_upShadow_iff` 📖	mathematical	—	`Finset` `instMembership` `upShadow` `instInsert`	—	—
`mem_upShadow_iff_erase_mem` 📖	mathematical	—	`Finset` `instMembership` `upShadow` `erase`	—	—
`mem_upShadow_iff_exists_mem_card_add` 📖	mathematical	—	`Finset` `instMembership` `Nat.iterate` `upShadow` `instHasSubset` `card`	—	`Subset.refl` `eq_of_subset_of_card_le` `Eq.ge` `mem_upShadow_iff_exists_mem_card_add_one` `HasSubset.Subset.trans` `instIsTransSubset` `add_right_comm` `exists_subsuperset_card_eq`
`mem_upShadow_iff_exists_mem_card_add_one` 📖	mathematical	—	`Finset` `instMembership` `upShadow` `instHasSubset` `card`	—	`mem_upShadow_iff_exists_sdiff` `card_sdiff_of_subset` `tsub_eq_iff_eq_add_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `card_mono` `add_comm`
`mem_upShadow_iff_exists_sdiff` 📖	mathematical	—	`Finset` `instMembership` `upShadow` `instHasSubset` `card` `instSDiff`	—	—
`mem_upShadow_iterate_iff_exists_card` 📖	mathematical	—	`Finset` `instMembership` `Nat.iterate` `upShadow` `card` `instHasSubset` `instSDiff`	—	`sdiff_empty` `Function.iterate_succ_apply'` `erase_sdiff_comm` `insert_subset` `insert_subset_iff`
`mem_upShadow_iterate_iff_exists_mem_card_add` 📖	mathematical	—	`Finset` `instMembership` `Nat.iterate` `upShadow` `instHasSubset` `card`	—	`mem_upShadow_iterate_iff_exists_sdiff` `card_sdiff_of_subset` `tsub_eq_iff_eq_add_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `card_mono` `add_comm`
`mem_upShadow_iterate_iff_exists_sdiff` 📖	mathematical	—	`Finset` `instMembership` `Nat.iterate` `upShadow` `instHasSubset` `card` `instSDiff`	—	`mem_upShadow_iterate_iff_exists_card` `sdiff_subset` `sdiff_sdiff_eq_self`
`shadow_compls` 📖	mathematical	—	`shadow` `compls` `Finset` `booleanAlgebra` `upShadow`	—	`ext` `compl_involutive` `Equiv.exists_congr_left` `compl_compl` `Function.Involutive.eq_iff` `compl_insert`
`shadow_empty` 📖	mathematical	—	`shadow` `Finset` `instEmptyCollection`	—	—
`shadow_iterate_empty` 📖	mathematical	—	`Nat.iterate` `Finset` `shadow` `instEmptyCollection`	—	—
`shadow_mono` 📖	mathematical	`Finset` `instHasSubset`	`shadow`	—	`shadow_monotone`
`shadow_monotone` 📖	mathematical	—	`Monotone` `Finset` `PartialOrder.toPreorder` `partialOrder` `shadow`	—	`sup_mono`
`shadow_singleton` 📖	mathematical	—	`shadow` `Finset` `instSingleton` `instEmptyCollection`	—	`sup_singleton` `image_singleton` `erase_singleton`
`shadow_singleton_empty` 📖	mathematical	—	`shadow` `Finset` `instSingleton` `instEmptyCollection`	—	—
`sized_shadow_iff` 📖	mathematical	`Finset` `instMembership` `instEmptyCollection`	`Set.Sized` `SetLike.coe` `instSetLike` `shadow`	—	`nonempty_iff_ne_empty` `erase_mem_shadow` `card_erase_add_one` `Set.Sized.shadow`
`upShadow_compls` 📖	mathematical	—	`upShadow` `compls` `Finset` `booleanAlgebra` `shadow`	—	`ext` `compl_involutive` `Equiv.exists_congr_left` `compl_compl` `Function.Involutive.eq_iff` `compl_erase`
`upShadow_empty` 📖	mathematical	—	`upShadow` `Finset` `instEmptyCollection`	—	—
`upShadow_monotone` 📖	mathematical	—	`Monotone` `Finset` `PartialOrder.toPreorder` `partialOrder` `upShadow`	—	`sup_mono`

FinsetFamily

Definitions

Name	Category	Theorems
`«term∂»` 📖	CompOp	—
`«term∂⁺»` 📖	CompOp	—

Set.Sized

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`shadow` 📖	mathematical	`Set.Sized` `SetLike.coe` `Finset` `Finset.instSetLike`	`Finset.shadow`	—	`Finset.mem_shadow_iff` `Finset.card_erase_of_mem`
`shadow_iterate` 📖	mathematical	`Set.Sized` `SetLike.coe` `Finset` `Finset.instSetLike`	`Nat.iterate` `Finset.shadow`	—	`Finset.card_sdiff_of_subset` `Finset.card_le_card`
`upShadow` 📖	mathematical	`Set.Sized` `SetLike.coe` `Finset` `Finset.instSetLike`	`Finset.upShadow`	—	`Finset.mem_upShadow_iff` `Finset.card_insert_of_notMem`

---

← Back to Index