Basic

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

Statistics

Metric	Count
Definitions union, piFinsetUnion, chooseX, equivToSet	4
Theorems union_inl, union_inr, union_symm_left, union_symm_right, piFinsetUnion_left, piFinsetUnion_right, attach, not_disjoint, not_empty_toList, toList_ne_nil, erase_nonempty, exists_cons_eq, attach_empty, attach_eq_empty_iff, attach_nonempty_iff, choose_mem, choose_property, choose_spec, disjUnion_eq_union, disjoint_disjUnion_left, disjoint_disjUnion_right, disjoint_erase_comm, disjoint_erase_insert, disjoint_filter, disjoint_filter_filter', disjoint_filter_filter_neg, disjoint_filter_filter_not, disjoint_insert_erase, disjoint_of_erase_left, disjoint_of_erase_right, disjoint_of_subset_iff_left_eq_empty, disjoint_or_nonempty_inter, disjoint_sdiff, disjoint_sdiff_inter, disjoint_union_left, disjoint_union_right, empty_toList, erase_cons, erase_cons_of_ne, erase_empty, erase_eq, erase_eq_empty_iff, erase_eq_iff_eq_insert, erase_injOn', erase_insert, erase_insert_eq_erase, erase_insert_of_ne, erase_insert_subset, erase_inter, erase_inter_comm, erase_nonempty, erase_sdiff_comm, erase_sdiff_distrib, erase_sdiff_erase, erase_singleton, erase_ssubset, erase_ssubset_insert, erase_subset_iff_of_mem, erase_union_distrib, erase_union_of_mem, filter_and, filter_and_not, filter_cons, filter_cons_of_neg, filter_cons_of_pos, filter_disjUnion, filter_eq, filter_eq', filter_erase, filter_insert, filter_inter, filter_inter_distrib, filter_mem_eq_inter, filter_ne, filter_ne', filter_not, filter_notMem_eq_sdiff, filter_or, filter_singleton, filter_union, filter_union_filter_neg_eq, filter_union_filter_not_eq, filter_union_filter_of_codisjoint, filter_union_right, insert_erase, insert_erase_invOn, insert_erase_subset, insert_inter_distrib, inter_erase, inter_filter, isDirected_le, isDirected_subset, isEmpty_of_forall_eq_empty, mem_union_of_disjoint, not_disjoint_iff_nonempty_inter, pairwiseDisjoint_iff, range_filter_eq, range_inter_range, range_union_range, sdiff_disjoint, sdiff_eq_filter, sdiff_erase, sdiff_erase_self, sdiff_insert, sdiff_insert_insert_of_mem_of_notMem, sdiff_singleton_eq_erase, sdiff_union_erase_cancel, ssubset_iff_exists_subset_erase, subset_insert_iff, subset_insert_iff_of_notMem, subset_union_elim, toList_empty, toList_eq_nil, union_erase_of_mem, univ_finset_eq_singleton_empty_iff, univ_finset_of_isEmpty, toFinset_nonempty_of_ne, toFinset_filter, toFinset_inter, toFinset_union, toFinset_nonempty_of_ne, toFinset_add, toFinset_eq_empty, toFinset_filter, toFinset_inter, toFinset_nonempty, toFinset_replicate, toFinset_union	128
Total	132

Equiv

Definitions

Name	Category	Theorems
piFinsetUnion 📖	CompOp	4 math math: Function.update_updateFinset, piFinsetUnion_right, Function.updateFinset_updateFinset, piFinsetUnion_left

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
piFinsetUnion_left 📖	mathematical	Disjoint Finset Finset.partialOrder Finset.instOrderBot Finset.instMembership Finset.instUnion	DFunLike.coe Equiv EquivLike.toFunLike instEquivLike piFinsetUnion SetLike.instMembership Finset.instSetLike	—	symm_apply_apply Finset.union_symm_left Mathlib.Tactic.DepRewrite.nddcongrArg
piFinsetUnion_right 📖	mathematical	Disjoint Finset Finset.partialOrder Finset.instOrderBot Finset.instMembership Finset.instUnion	DFunLike.coe Equiv EquivLike.toFunLike instEquivLike piFinsetUnion SetLike.instMembership Finset.instSetLike	—	symm_apply_apply Finset.union_symm_right Mathlib.Tactic.DepRewrite.nddcongrArg

Equiv.Finset

Definitions

Name	Category	Theorems
union 📖	CompOp	4 math math: union_inl, union_symm_left, union_symm_right, union_inr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
union_inl 📖	mathematical	Disjoint Finset Finset.partialOrder Finset.instOrderBot	DFunLike.coe Equiv SetLike.instMembership Finset.instSetLike Finset.instUnion EquivLike.toFunLike Equiv.instEquivLike union Finset.instMembership Finset.mem_union	—	—
union_inr 📖	mathematical	Disjoint Finset Finset.partialOrder Finset.instOrderBot	DFunLike.coe Equiv SetLike.instMembership Finset.instSetLike Finset.instUnion EquivLike.toFunLike Equiv.instEquivLike union Finset.instMembership Finset.mem_union	—	—
union_symm_left 📖	mathematical	Disjoint Finset Finset.partialOrder Finset.instOrderBot Finset.instMembership Finset.instUnion	DFunLike.coe Equiv SetLike.instMembership Finset.instSetLike EquivLike.toFunLike Equiv.instEquivLike Equiv.symm union	—	—
union_symm_right 📖	mathematical	Disjoint Finset Finset.partialOrder Finset.instOrderBot Finset.instMembership Finset.instUnion	DFunLike.coe Equiv SetLike.instMembership Finset.instSetLike EquivLike.toFunLike Equiv.instEquivLike Equiv.symm union	—	—

Finset

Definitions

Name	Category	Theorems
chooseX 📖	CompOp	—
equivToSet 📖	CompOp	2 math math: piCongrLeft_comp_restrict, Set.piCongrLeft_comp_restrict

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
attach_empty 📖	mathematical	—	attach Finset instEmptyCollection instMembership	—	—
attach_eq_empty_iff 📖	mathematical	—	attach Finset instMembership instEmptyCollection	—	—
attach_nonempty_iff 📖	mathematical	—	Nonempty Finset instMembership attach	—	—
choose_mem 📖	mathematical	ExistsUnique Finset instMembership	choose	—	choose_spec
choose_property 📖	mathematical	ExistsUnique Finset instMembership	choose	—	choose_spec
choose_spec 📖	mathematical	ExistsUnique Finset instMembership	choose	—	—
disjUnion_eq_union 📖	mathematical	Disjoint Finset partialOrder instOrderBot	disjUnion instUnion	—	—
disjoint_disjUnion_left 📖	mathematical	Disjoint Finset partialOrder instOrderBot	disjUnion	—	—
disjoint_disjUnion_right 📖	mathematical	Disjoint Finset partialOrder instOrderBot	disjUnion	—	—
disjoint_erase_comm 📖	mathematical	—	Disjoint Finset partialOrder instOrderBot erase	—	erase_eq
disjoint_erase_insert 📖	mathematical	Finset instMembership	Disjoint partialOrder instOrderBot instInsert erase	—	disjoint_erase_comm erase_insert
disjoint_filter 📖	mathematical	—	Disjoint Finset partialOrder instOrderBot filter	—	—
disjoint_filter_filter' 📖	mathematical	Disjoint Pi.partialOrder Prop.partialOrder Pi.instOrderBot Prop.le HeytingAlgebra.toOrderBot Prop.instHeytingAlgebra	Finset partialOrder instOrderBot filter	—	Pi.disjoint_iff
disjoint_filter_filter_neg 📖	mathematical	—	Disjoint Finset partialOrder instOrderBot filter	—	disjoint_filter_filter_not
disjoint_filter_filter_not 📖	mathematical	—	Disjoint Finset partialOrder instOrderBot filter	—	disjoint_filter_filter' disjoint_compl_right
disjoint_insert_erase 📖	mathematical	Finset instMembership	Disjoint partialOrder instOrderBot erase instInsert	—	disjoint_erase_comm erase_insert
disjoint_of_erase_left 📖	—	Finset instMembership Disjoint partialOrder instOrderBot erase	—	—	erase_insert disjoint_erase_comm disjoint_insert_right notMem_erase
disjoint_of_erase_right 📖	—	Finset instMembership Disjoint partialOrder instOrderBot erase	—	—	erase_insert disjoint_erase_comm disjoint_insert_left notMem_erase
disjoint_of_subset_iff_left_eq_empty 📖	mathematical	Finset instHasSubset	Disjoint partialOrder instOrderBot instEmptyCollection	—	disjoint_of_le_iff_left_eq_bot
disjoint_or_nonempty_inter 📖	mathematical	—	Disjoint Finset partialOrder instOrderBot Nonempty instInter	—	not_disjoint_iff_nonempty_inter em
disjoint_sdiff 📖	mathematical	—	Disjoint Finset partialOrder instOrderBot instSDiff	—	Disjoint.symm sdiff_disjoint
disjoint_sdiff_inter 📖	mathematical	—	Disjoint Finset partialOrder instOrderBot instSDiff instInter	—	disjoint_of_subset_right inter_subset_right sdiff_disjoint
disjoint_union_left 📖	mathematical	—	Disjoint Finset partialOrder instOrderBot instUnion	—	—
disjoint_union_right 📖	mathematical	—	Disjoint Finset partialOrder instOrderBot instUnion	—	—
empty_toList 📖	mathematical	—	toList Finset instEmptyCollection	—	—
erase_cons 📖	mathematical	Finset instMembership	erase cons	—	—
erase_cons_of_ne 📖	mathematical	Finset instMembership	erase cons erase_subset	—	—
erase_empty 📖	mathematical	—	erase Finset instEmptyCollection	—	—
erase_eq 📖	mathematical	—	erase Finset instSDiff instSingleton	—	sdiff_singleton_eq_erase
erase_eq_empty_iff 📖	mathematical	—	erase Finset instEmptyCollection instSingleton	—	sdiff_singleton_eq_erase sdiff_eq_empty_iff_subset subset_singleton_iff
erase_eq_iff_eq_insert 📖	mathematical	Finset instMembership	erase instInsert	—	insert_erase erase_insert_eq_erase erase_eq_of_notMem
erase_injOn' 📖	mathematical	—	Set.InjOn Finset erase setOf instMembership	—	insert_erase
erase_insert 📖	mathematical	Finset instMembership	erase instInsert	—	—
erase_insert_eq_erase 📖	mathematical	—	erase Finset instInsert	—	—
erase_insert_of_ne 📖	mathematical	—	erase Finset instInsert	—	—
erase_insert_subset 📖	mathematical	—	Finset instHasSubset erase instInsert	—	subset_insert_iff Subset.rfl
erase_inter 📖	mathematical	—	Finset instInter erase	—	—
erase_inter_comm 📖	mathematical	—	Finset instInter erase	—	—
erase_nonempty 📖	mathematical	Finset instMembership	Nonempty erase Nontrivial	—	Nontrivial.exists_ne
erase_sdiff_comm 📖	mathematical	—	Finset instSDiff erase	—	—
erase_sdiff_distrib 📖	mathematical	—	erase Finset instSDiff	—	—
erase_sdiff_erase 📖	mathematical	Finset instMembership	instSDiff erase instSingleton	—	ext
erase_singleton 📖	mathematical	—	erase Finset instSingleton instEmptyCollection	—	—
erase_ssubset 📖	mathematical	Finset instMembership	instHasSSubset erase	—	—
erase_ssubset_insert 📖	mathematical	—	Finset instHasSSubset erase instInsert	—	ssubset_iff_exists_subset_erase mem_insert_self Mathlib.Tactic.GCongr.rel_imp_rel instIsTransSubset subset_refl instReflSubset erase_subset_erase subset_insert
erase_subset_iff_of_mem 📖	mathematical	Finset instMembership	instHasSubset erase	—	subset_insert_iff insert_eq_of_mem
erase_union_distrib 📖	mathematical	—	erase Finset instUnion	—	—
erase_union_of_mem 📖	mathematical	Finset instMembership	instUnion erase	—	—
filter_and 📖	mathematical	—	filter Finset instInter	—	—
filter_and_not 📖	mathematical	—	filter Finset instSDiff	—	—
filter_cons 📖	mathematical	Finset instMembership	filter cons Function.mt mem_of_mem_filter	—	—
filter_cons_of_neg 📖	mathematical	Finset instMembership	filter cons	—	eq_of_veq Multiset.filter_cons_of_neg
filter_cons_of_pos 📖	mathematical	Finset instMembership	filter cons Function.mt mem_of_mem_filter	—	eq_of_veq Function.mt mem_of_mem_filter Multiset.filter_cons_of_pos
filter_disjUnion 📖	mathematical	Disjoint Finset partialOrder instOrderBot	filter disjUnion disjoint_filter_filter	—	eq_of_veq disjoint_filter_filter Multiset.filter_add
filter_eq 📖	mathematical	—	filter Finset instMembership decidableMem instSingleton instEmptyCollection	—	—
filter_eq' 📖	mathematical	—	filter Finset instMembership decidableMem instSingleton instEmptyCollection	—	—
filter_erase 📖	mathematical	—	filter erase	—	—
filter_insert 📖	mathematical	—	filter Finset instInsert	—	—
filter_inter 📖	mathematical	—	Finset instInter filter	—	—
filter_inter_distrib 📖	mathematical	—	filter Finset instInter	—	—
filter_mem_eq_inter 📖	mathematical	—	filter Finset instMembership instInter	—	—
filter_ne 📖	mathematical	—	filter erase	—	—
filter_ne' 📖	mathematical	—	filter erase	—	filter_congr filter_ne
filter_not 📖	mathematical	—	filter Finset instSDiff	—	—
filter_notMem_eq_sdiff 📖	mathematical	—	filter Finset instMembership instSDiff	—	—
filter_or 📖	mathematical	—	filter Finset instUnion	—	—
filter_singleton 📖	mathematical	—	filter Finset instSingleton instEmptyCollection	—	—
filter_union 📖	mathematical	—	filter Finset instUnion	—	—
filter_union_filter_neg_eq 📖	mathematical	—	Finset instUnion filter	—	filter_union_filter_not_eq
filter_union_filter_not_eq 📖	mathematical	—	Finset instUnion filter	—	filter_union_filter_of_codisjoint codisjoint_hnot_right
filter_union_filter_of_codisjoint 📖	mathematical	Codisjoint Pi.partialOrder Prop.partialOrder Pi.instOrderTop Prop.le CoheytingAlgebra.toOrderTop BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra Prop.instBooleanAlgebra	Finset instUnion filter	—	filter_or filter_true_of_mem Codisjoint.top_le
filter_union_right 📖	mathematical	—	Finset instUnion filter	—	—
insert_erase 📖	mathematical	Finset instMembership	instInsert erase	—	—
insert_erase_invOn 📖	mathematical	—	Set.InvOn Finset instInsert erase setOf instMembership	—	insert_erase erase_insert
insert_erase_subset 📖	mathematical	—	Finset instHasSubset instInsert erase	—	subset_insert_iff Subset.rfl
insert_inter_distrib 📖	mathematical	—	Finset instInsert instInter	—	—
inter_erase 📖	mathematical	—	Finset instInter erase	—	—
inter_filter 📖	mathematical	—	Finset instInter filter	—	—
isDirected_le 📖	mathematical	—	IsDirectedOrder Finset Preorder.toLE PartialOrder.toPreorder partialOrder	—	SemilatticeSup.instIsDirectedOrder
isDirected_subset 📖	mathematical	—	IsDirected Finset instHasSubset	—	isDirected_le
isEmpty_of_forall_eq_empty 📖	mathematical	Finset instEmptyCollection	IsEmpty	—	isEmpty_iff
mem_union_of_disjoint 📖	mathematical	Disjoint Finset partialOrder instOrderBot	instMembership instUnion Xor'	—	mem_union Xor'.eq_1 disjoint_left
not_disjoint_iff_nonempty_inter 📖	mathematical	—	Disjoint Finset partialOrder instOrderBot Nonempty instInter	—	not_disjoint_iff
pairwiseDisjoint_iff 📖	mathematical	—	Set.PairwiseDisjoint Finset partialOrder instOrderBot	—	not_imp_comm
range_filter_eq 📖	mathematical	—	filter range Finset instSingleton instEmptyCollection	—	—
range_inter_range 📖	mathematical	—	Finset instInter range	—	ext
range_union_range 📖	mathematical	—	Finset instUnion range	—	ext
sdiff_disjoint 📖	mathematical	—	Disjoint Finset partialOrder instOrderBot instSDiff	—	disjoint_left mem_sdiff
sdiff_eq_filter 📖	mathematical	—	Finset instSDiff filter instMembership decidableMem	—	—
sdiff_erase 📖	mathematical	Finset instMembership	instSDiff erase instInsert	—	—
sdiff_erase_self 📖	mathematical	Finset instMembership	instSDiff erase instSingleton	—	—
sdiff_insert 📖	mathematical	—	Finset instSDiff instInsert erase	—	—
sdiff_insert_insert_of_mem_of_notMem 📖	mathematical	Finset instMembership	instInsert instSDiff	—	—
sdiff_singleton_eq_erase 📖	mathematical	—	Finset instSDiff instSingleton erase	—	—
sdiff_union_erase_cancel 📖	mathematical	Finset instHasSubset instMembership	instUnion instSDiff erase	—	—
ssubset_iff_exists_subset_erase 📖	mathematical	—	Finset instHasSSubset instMembership instHasSubset erase	—	—
subset_insert_iff 📖	mathematical	—	Finset instHasSubset instInsert erase	—	—
subset_insert_iff_of_notMem 📖	mathematical	Finset instMembership	instHasSubset instInsert	—	subset_insert_iff erase_eq_of_notMem
subset_union_elim 📖	mathematical	Set Set.instHasSubset SetLike.coe Finset instSetLike Set.instUnion	instUnion Set.instSDiff	—	coe_filter
toList_empty 📖	mathematical	—	toList Finset instEmptyCollection	—	toList_eq_nil
toList_eq_nil 📖	mathematical	—	toList Finset instEmptyCollection	—	Multiset.toList_eq_nil val_eq_zero
union_erase_of_mem 📖	mathematical	Finset instMembership	instUnion erase	—	—
univ_finset_eq_singleton_empty_iff 📖	mathematical	—	Set.univ Finset Set Set.instSingletonSet instEmptyCollection IsEmpty	—	isEmpty_of_forall_eq_empty Set.mem_singleton_iff Set.ext_iff Set.mem_univ univ_finset_of_isEmpty
univ_finset_of_isEmpty 📖	mathematical	—	Set.univ Finset Set Set.instSingletonSet instEmptyCollection	—	subset_antisymm Set.instAntisymmSubset eq_empty_of_isEmpty

Finset.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
attach 📖	mathematical	Finset.Nonempty	Finset Finset.instMembership Finset.attach	—	Finset.attach_nonempty_iff
not_disjoint 📖	mathematical	Finset.Nonempty Finset Finset.instInter	Disjoint Finset.partialOrder Finset.instOrderBot	—	Finset.not_disjoint_iff_nonempty_inter
not_empty_toList 📖	mathematical	Finset.Nonempty	Finset.toList	—	Finset.empty_toList ne_empty
toList_ne_nil 📖	—	Finset.Nonempty	—	—	Finset.toList_eq_nil ne_empty

Finset.Nontrivial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
erase_nonempty 📖	mathematical	Finset.Nontrivial	Finset.Nonempty Finset.erase	—	exists_ne
exists_cons_eq 📖	mathematical	Finset.Nontrivial	Finset.cons Finset Finset.instMembership Iff.not Finset.mem_cons	—	Iff.not Finset.mem_cons Finset.mem_erase Finset.cons_eq_insert Finset.insert_erase Finset.cons.congr_simp

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toFinset_filter 📖	mathematical	—	toFinset Finset.filter	—	Finset.ext
toFinset_inter 📖	mathematical	—	toFinset Finset Finset.instInter	—	Finset.ext
toFinset_union 📖	mathematical	—	toFinset Finset Finset.instUnion	—	Finset.ext

List.Aesop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toFinset_nonempty_of_ne 📖	mathematical	—	Finset.Nonempty List.toFinset	—	List.toFinset_nonempty_iff

Multiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toFinset_add 📖	mathematical	—	toFinset Multiset instAdd Finset Finset.instUnion	—	Finset.ext
toFinset_eq_empty 📖	mathematical	—	toFinset Finset Finset.instEmptyCollection Multiset instZero	—	dedup_eq_zero
toFinset_filter 📖	mathematical	—	toFinset filter Finset.filter	—	Finset.ext
toFinset_inter 📖	mathematical	—	toFinset Multiset instInter Finset Finset.instInter	—	Finset.ext
toFinset_nonempty 📖	mathematical	—	Finset.Nonempty toFinset	—	—
toFinset_replicate 📖	mathematical	—	toFinset replicate Finset Finset.instEmptyCollection Finset.instSingleton	—	Finset.ext
toFinset_union 📖	mathematical	—	toFinset Multiset instUnion Finset Finset.instUnion	—	Finset.ext

Multiset.Aesop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toFinset_nonempty_of_ne 📖	mathematical	—	Finset.Nonempty Multiset.toFinset	—	Multiset.toFinset_nonempty

---

← Back to Index