Slice

📁 Source: Mathlib/Data/Finset/Slice.lean

Statistics

Metric	Count
Definitions slice, «term_#_», Sized	3
Theorems biUnion_slice, eq_of_mem_slice, mem_slice, ne_of_mem_slice, pairwiseDisjoint_slice, sized_slice, slice_subset, subset_powersetCard_univ_iff, sum_card_slice, card_le, empty_mem_iff, isAntichain, mono, subset_powersetCard_univ, subsingleton, subsingleton', univ_mem_iff, union, sized_empty, sized_iUnion, sized_iUnion₂, sized_powersetCard, sized_singleton, sized_union	24
Total	27

Finset

Definitions

Name	Category	Theorems
slice 📖	CompOp	12 math math: slice_subset, lubell_yamamoto_meshalkin_inequality_sum_card_div_choose, slice_subset_falling, sized_slice, biUnion_slice, sum_card_slice, le_card_falling_div_choose, sum_card_slice_div_choose_le_one, slice_union_shadow_falling_succ, mem_slice, pairwiseDisjoint_slice, IsAntichain.disjoint_slice_shadow_falling
«term_#_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biUnion_slice 📖	mathematical	—	biUnion Finset decidableEq Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder Fintype.card slice	—	Subset.antisymm biUnion_subset slice_subset mem_biUnion mem_Iic card_le_univ mem_slice
eq_of_mem_slice 📖	—	Finset instMembership slice	—	—	sized_slice
mem_slice 📖	mathematical	—	Finset instMembership slice card	—	mem_filter
ne_of_mem_slice 📖	—	Finset instMembership slice	—	—	sized_slice
pairwiseDisjoint_slice 📖	mathematical	—	Set.PairwiseDisjoint Finset partialOrder instOrderBot Set.univ slice	—	disjoint_filter
sized_slice 📖	mathematical	—	Set.Sized SetLike.coe Finset instSetLike slice	—	mem_slice
slice_subset 📖	mathematical	—	Finset instHasSubset slice	—	filter_subset
subset_powersetCard_univ_iff 📖	mathematical	—	Finset instHasSubset powersetCard univ Set.Sized SetLike.coe instSetLike	—	mem_powersetCard_univ mem_coe
sum_card_slice 📖	mathematical	—	sum Nat.instAddCommMonoid Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder Fintype.card card Finset slice	—	card_biUnion Set.PairwiseDisjoint.subset pairwiseDisjoint_slice Set.subset_univ biUnion_slice

Set

Definitions

Name	Category	Theorems
Sized 📖	MathDef	11 math math: Finset.sized_compls, Finset.sized_slice, Finset.subset_powersetCard_univ_iff, sized_iUnion₂, Finset.sized_shadow_iff, sized_singleton, Finset.sized_falling, sized_iUnion, sized_empty, sized_powersetCard, sized_union

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sized_empty 📖	mathematical	—	Sized Set Finset instEmptyCollection	—	instIsEmptyFalse
sized_iUnion 📖	mathematical	—	Sized iUnion Finset	—	forall_swap
sized_iUnion₂ 📖	mathematical	—	Sized iUnion Finset	—	—
sized_powersetCard 📖	mathematical	—	Sized SetLike.coe Finset Finset.instSetLike Finset.powersetCard	—	Finset.mem_powersetCard
sized_singleton 📖	mathematical	—	Sized Finset Set instSingletonSet Finset.card	—	—
sized_union 📖	mathematical	—	Sized Set Finset instUnion	—	Sized.mono subset_union_left subset_union_right

Set.Sized

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_le 📖	mathematical	Set.Sized SetLike.coe Finset Finset.instSetLike	Finset.card Nat.choose Fintype.card	—	Fintype.card.eq_1 Finset.card_powersetCard Finset.card_le_card Finset.subset_powersetCard_univ_iff
empty_mem_iff 📖	mathematical	Set.Sized	Finset Set Set.instMembership Finset.instEmptyCollection Set.instSingletonSet	—	IsAntichain.bot_mem_iff isAntichain
isAntichain 📖	mathematical	Set.Sized	IsAntichain Finset Finset.instHasSubset	—	Finset.eq_of_subset_of_card_le Eq.le
mono 📖	—	Set Finset Set.instHasSubset Set.Sized	—	—	—
subset_powersetCard_univ 📖	mathematical	Set.Sized SetLike.coe Finset Finset.instSetLike	Finset.instHasSubset Finset.powersetCard Finset.univ	—	Finset.subset_powersetCard_univ_iff
subsingleton 📖	mathematical	Set.Sized	Set.Subsingleton Finset	—	Set.subsingleton_of_forall_eq Finset.card_eq_zero
subsingleton' 📖	mathematical	Set.Sized Fintype.card	Set.Subsingleton Finset	—	Set.subsingleton_of_forall_eq Finset.card_eq_iff_eq_univ
univ_mem_iff 📖	mathematical	Set.Sized	Finset Set Set.instMembership Finset.univ Set.instSingletonSet	—	IsAntichain.top_mem_iff isAntichain

Set.sized

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
union 📖	mathematical	Set.Sized	Set Finset Set.instUnion	—	Set.sized_union

---

← Back to Index