Down

📁 Source: Mathlib/Combinatorics/SetFamily/Compression/Down.lean

Statistics

Metric	Count
Definitions compression, memberSubfamily, nonMemberSubfamily, term𝓓	4
Theorems card_compression, compression_idem, erase_mem_compression, erase_mem_compression_of_mem_compression, mem_compression, mem_compression_of_insert_mem_compression, card_memberSubfamily_add_card_nonMemberSubfamily, family_induction_on, image_insert_memberSubfamily, mem_memberSubfamily, mem_nonMemberSubfamily, memberFamily_induction_on, memberSubfamily_image_erase, memberSubfamily_image_insert, memberSubfamily_inter, memberSubfamily_memberSubfamily, memberSubfamily_nonMemberSubfamily, memberSubfamily_union, memberSubfamily_union_nonMemberSubfamily, nonMemberSubfamily_image_insert, nonMemberSubfamily_inter, nonMemberSubfamily_memberSubfamily, nonMemberSubfamily_nonMemberSubfamily, nonMemberSubfamily_union	24
Total	28

Down

Definitions

Name	Category	Theorems
compression 📖	CompOp	6 math math: Finset.shatterer_compress_subset_shatterer, card_compression, Finset.vcDim_compress_le, compression_idem, mem_compression, erase_mem_compression

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_compression 📖	mathematical	—	Finset.card Finset compression	—	compression.eq_1 Finset.card_disjUnion Finset.filter_image Finset.card_image_of_injOn Set.InjOn.mono not_imp_comm Finset.erase_eq_of_notMem Finset.mem_filter Finset.mem_coe Finset.erase_injOn' Finset.card_union_of_disjoint Finset.disjoint_filter_filter_not Finset.filter_union_filter_not_eq
compression_idem 📖	mathematical	—	compression	—	Finset.ext mem_compression mem_compression_of_insert_mem_compression erase_mem_compression_of_mem_compression
erase_mem_compression 📖	mathematical	Finset Finset.instMembership	compression Finset.erase	—	Finset.erase_idem Finset.insert_erase Finset.erase_ne_self em
erase_mem_compression_of_mem_compression 📖	mathematical	Finset Finset.instMembership compression	Finset.erase	—	Finset.erase_idem Finset.erase_eq_of_notMem Finset.insert_ne_self
mem_compression 📖	mathematical	—	Finset Finset.instMembership compression Finset.erase Finset.instInsert	—	Finset.insert_erase Finset.erase_ne_self Finset.erase_insert Finset.insert_ne_self
mem_compression_of_insert_mem_compression 📖	—	Finset Finset.instMembership compression Finset.instInsert	—	—	Finset.insert_eq_of_mem Finset.erase_insert erase_mem_compression_of_mem_compression

Finset

Definitions

Name	Category	Theorems
memberSubfamily 📖	CompOp	13 math math: card_memberSubfamily_add_card_nonMemberSubfamily, memberSubfamily_image_erase, IsLowerSet.memberSubfamily, nonMemberSubfamily_memberSubfamily, memberSubfamily_inter, memberSubfamily_nonMemberSubfamily, memberSubfamily_image_insert, memberSubfamily_union_nonMemberSubfamily, IsLowerSet.memberSubfamily_subset_nonMemberSubfamily, image_insert_memberSubfamily, mem_memberSubfamily, memberSubfamily_memberSubfamily, memberSubfamily_union
nonMemberSubfamily 📖	CompOp	11 math math: card_memberSubfamily_add_card_nonMemberSubfamily, nonMemberSubfamily_union, nonMemberSubfamily_memberSubfamily, nonMemberSubfamily_inter, nonMemberSubfamily_image_insert, mem_nonMemberSubfamily, memberSubfamily_nonMemberSubfamily, IsLowerSet.nonMemberSubfamily, memberSubfamily_union_nonMemberSubfamily, nonMemberSubfamily_nonMemberSubfamily, IsLowerSet.memberSubfamily_subset_nonMemberSubfamily

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_memberSubfamily_add_card_nonMemberSubfamily 📖	mathematical	—	card Finset memberSubfamily nonMemberSubfamily	—	memberSubfamily.eq_1 nonMemberSubfamily.eq_1 card_image_of_injOn Set.InjOn.mono erase_injOn' coe_filter card_filter_add_card_filter_not
family_induction_on 📖	—	Finset instEmptyCollection instSingleton image decidableEq instInsert	—	—	memberFamily_induction_on image_insert_memberSubfamily
image_insert_memberSubfamily 📖	mathematical	—	image Finset decidableEq instInsert memberSubfamily filter instMembership decidableMem	—	ext mem_insert_self insert_erase notMem_erase
mem_memberSubfamily 📖	mathematical	—	Finset instMembership memberSubfamily instInsert	—	insert_erase notMem_erase erase_insert
mem_nonMemberSubfamily 📖	mathematical	—	Finset instMembership nonMemberSubfamily	—	—
memberFamily_induction_on 📖	—	Finset instEmptyCollection instSingleton	—	—	le_sup induction subset_singleton_iff subset_singleton_iff' subset_insert_iff_of_notMem insert_subset_insert_iff
memberSubfamily_image_erase 📖	mathematical	—	memberSubfamily image Finset decidableEq erase instEmptyCollection	—	mem_insert_self notMem_erase
memberSubfamily_image_insert 📖	mathematical	Finset instMembership	memberSubfamily image decidableEq instInsert	—	ext Set.LeftInvOn.injOn insert_erase_invOn
memberSubfamily_inter 📖	mathematical	—	memberSubfamily Finset instInter decidableEq	—	filter_inter_distrib image_inter_of_injOn Set.InjOn.mono coe_filter erase_injOn'
memberSubfamily_memberSubfamily 📖	mathematical	—	memberSubfamily Finset instEmptyCollection	—	ext insert_eq_of_mem
memberSubfamily_nonMemberSubfamily 📖	mathematical	—	memberSubfamily nonMemberSubfamily Finset instEmptyCollection	—	ext
memberSubfamily_union 📖	mathematical	—	memberSubfamily Finset instUnion decidableEq	—	filter_union image_union
memberSubfamily_union_nonMemberSubfamily 📖	mathematical	—	Finset instUnion decidableEq memberSubfamily nonMemberSubfamily image erase	—	ext erase_insert erase_eq_of_notMem insert_erase notMem_erase
nonMemberSubfamily_image_insert 📖	mathematical	—	nonMemberSubfamily image Finset decidableEq instInsert instEmptyCollection	—	—
nonMemberSubfamily_inter 📖	mathematical	—	nonMemberSubfamily Finset instInter decidableEq	—	filter_inter_distrib
nonMemberSubfamily_memberSubfamily 📖	mathematical	—	nonMemberSubfamily memberSubfamily	—	ext
nonMemberSubfamily_nonMemberSubfamily 📖	mathematical	—	nonMemberSubfamily	—	ext
nonMemberSubfamily_union 📖	mathematical	—	nonMemberSubfamily Finset instUnion decidableEq	—	filter_union

FinsetFamily

Definitions

Name	Category	Theorems
term𝓓 📖	CompOp	—

---

← Back to Index