Basic

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

Statistics

Metric	Count
Definitions `disjUnionEquiv`, `union`, `piFinsetUnion`, `chooseX`, `equivToSet`	5
Theorems `disjUnionEquiv_inl`, `disjUnionEquiv_inr`, `disjUnionEquiv_symm_left`, `disjUnionEquiv_symm_right`, `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`	132
Total	137

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` `SetLike.instMembership` `Finset.instSetLike` `Finset.instUnion`	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `piFinsetUnion` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.instUnion`	—	`symm_apply_apply` `Finset.union_symm_left` `Mathlib.Tactic.DepRewrite.nddcongrArg`
`piFinsetUnion_right` 📖	mathematical	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `SetLike.instMembership` `Finset.instSetLike` `Finset.instUnion`	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `piFinsetUnion` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.instUnion`	—	`symm_apply_apply` `Finset.union_symm_right` `Mathlib.Tactic.DepRewrite.nddcongrArg`

Equiv.Finset

Definitions

Name	Category	Theorems
`disjUnionEquiv` 📖	CompOp	4 math math: `disjUnionEquiv_symm_right`, `disjUnionEquiv_inr`, `disjUnionEquiv_symm_left`, `disjUnionEquiv_inl`
`union` 📖	CompOp	4 math math: `union_inl`, `union_symm_left`, `union_symm_right`, `union_inr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjUnionEquiv_inl` 📖	mathematical	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot`	`DFunLike.coe` `Equiv` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.disjUnion` `EquivLike.toFunLike` `Equiv.instEquivLike` `disjUnionEquiv` `Finset.mem_disjUnion`	—	—
`disjUnionEquiv_inr` 📖	mathematical	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot`	`DFunLike.coe` `Equiv` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.disjUnion` `EquivLike.toFunLike` `Equiv.instEquivLike` `disjUnionEquiv` `Finset.mem_disjUnion`	—	—
`disjUnionEquiv_symm_left` 📖	mathematical	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `SetLike.instMembership` `Finset.instSetLike` `Finset.disjUnion`	`DFunLike.coe` `Equiv` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.disjUnion` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `disjUnionEquiv`	—	—
`disjUnionEquiv_symm_right` 📖	mathematical	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `SetLike.instMembership` `Finset.instSetLike` `Finset.disjUnion`	`DFunLike.coe` `Equiv` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.disjUnion` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `disjUnionEquiv`	—	—
`union_inl` 📖	mathematical	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot`	`DFunLike.coe` `Equiv` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.instUnion` `EquivLike.toFunLike` `Equiv.instEquivLike` `union` `Finset.mem_union`	—	—
`union_inr` 📖	mathematical	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot`	`DFunLike.coe` `Equiv` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.instUnion` `EquivLike.toFunLike` `Equiv.instEquivLike` `union` `Finset.mem_union`	—	—
`union_symm_left` 📖	mathematical	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `SetLike.instMembership` `Finset.instSetLike` `Finset.instUnion`	`DFunLike.coe` `Equiv` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.instUnion` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `union`	—	—
`union_symm_right` 📖	mathematical	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `SetLike.instMembership` `Finset.instSetLike` `Finset.instUnion`	`DFunLike.coe` `Equiv` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.instUnion` `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` `SetLike.instMembership` `instSetLike`	—	—
`attach_eq_empty_iff` 📖	mathematical	—	`attach` `Finset` `SetLike.instMembership` `instSetLike` `instEmptyCollection`	—	—
`attach_nonempty_iff` 📖	mathematical	—	`Nonempty` `Finset` `SetLike.instMembership` `instSetLike` `attach`	—	—
`choose_mem` 📖	mathematical	`ExistsUnique` `Finset` `SetLike.instMembership` `instSetLike`	`Finset` `SetLike.instMembership` `instSetLike` `choose`	—	`choose_spec`
`choose_property` 📖	mathematical	`ExistsUnique` `Finset` `SetLike.instMembership` `instSetLike`	`choose`	—	`choose_spec`
`choose_spec` 📖	mathematical	`ExistsUnique` `Finset` `SetLike.instMembership` `instSetLike`	`Finset` `SetLike.instMembership` `instSetLike` `choose`	—	—
`disjUnion_eq_union` 📖	mathematical	`Disjoint` `Finset` `partialOrder` `instOrderBot`	`disjUnion` `Finset` `instUnion`	—	—
`disjoint_disjUnion_left` 📖	mathematical	`Disjoint` `Finset` `partialOrder` `instOrderBot`	`Disjoint` `Finset` `partialOrder` `instOrderBot` `disjUnion`	—	—
`disjoint_disjUnion_right` 📖	mathematical	`Disjoint` `Finset` `partialOrder` `instOrderBot`	`Disjoint` `Finset` `partialOrder` `instOrderBot` `disjUnion`	—	—
`disjoint_erase_comm` 📖	mathematical	—	`Disjoint` `Finset` `partialOrder` `instOrderBot` `erase`	—	`erase_eq`
`disjoint_erase_insert` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike`	`Disjoint` `Finset` `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`	`Disjoint` `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` `SetLike.instMembership` `instSetLike`	`Disjoint` `Finset` `partialOrder` `instOrderBot` `erase` `instInsert`	—	`disjoint_erase_comm` `erase_insert`
`disjoint_of_erase_left` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike` `Disjoint` `partialOrder` `instOrderBot` `erase`	`Disjoint` `Finset` `partialOrder` `instOrderBot`	—	`erase_insert` `disjoint_erase_comm` `disjoint_insert_right` `notMem_erase`
`disjoint_of_erase_right` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike` `Disjoint` `partialOrder` `instOrderBot` `erase`	`Disjoint` `Finset` `partialOrder` `instOrderBot`	—	`erase_insert` `disjoint_erase_comm` `disjoint_insert_left` `notMem_erase`
`disjoint_of_subset_iff_left_eq_empty` 📖	mathematical	`Finset` `instHasSubset`	`Disjoint` `Finset` `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` `SetLike.instMembership` `instSetLike`	`erase` `cons`	—	—
`erase_cons_of_ne` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike`	`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` `SetLike.instMembership` `instSetLike`	`erase` `Finset` `instInsert`	—	`insert_erase` `erase_insert_eq_erase` `erase_eq_of_notMem`
`erase_injOn'` 📖	mathematical	—	`Set.InjOn` `Finset` `erase` `setOf` `SetLike.instMembership` `instSetLike`	—	`insert_erase`
`erase_insert` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike`	`erase` `Finset` `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` `SetLike.instMembership` `instSetLike`	`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` `SetLike.instMembership` `instSetLike`	`Finset` `instSDiff` `erase` `instSingleton`	—	`ext`
`erase_singleton` 📖	mathematical	—	`erase` `Finset` `instSingleton` `instEmptyCollection`	—	—
`erase_ssubset` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike`	`Finset` `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` `SetLike.instMembership` `instSetLike`	`Finset` `instHasSubset` `erase`	—	`subset_insert_iff` `insert_eq_of_mem`
`erase_union_distrib` 📖	mathematical	—	`erase` `Finset` `instUnion`	—	—
`erase_union_of_mem` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike`	`Finset` `instUnion` `erase`	—	—
`filter_and` 📖	mathematical	—	`filter` `Finset` `instInter`	—	—
`filter_and_not` 📖	mathematical	—	`filter` `Finset` `instSDiff`	—	—
`filter_cons` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike`	`filter` `cons` `Finset` `Function.mt` `SetLike.instMembership` `instSetLike` `mem_of_mem_filter`	—	—
`filter_cons_of_neg` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike`	`filter` `cons`	—	`eq_of_veq` `Multiset.filter_cons_of_neg`
`filter_cons_of_pos` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike`	`filter` `cons` `Function.mt` `Finset` `SetLike.instMembership` `instSetLike` `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` `SetLike.instMembership` `instSetLike` `decidableMem` `instSingleton` `instEmptyCollection`	—	—
`filter_eq'` 📖	mathematical	—	`filter` `Finset` `SetLike.instMembership` `instSetLike` `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` `SetLike.instMembership` `instSetLike` `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` `SetLike.instMembership` `instSetLike` `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` `SetLike.instMembership` `instSetLike`	`Finset` `instInsert` `erase`	—	—
`insert_erase_invOn` 📖	mathematical	—	`Set.InvOn` `Finset` `instInsert` `erase` `setOf` `SetLike.instMembership` `instSetLike`	—	`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`	`Finset` `SetLike.instMembership` `instSetLike` `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` `SetLike.instMembership` `instSetLike` `decidableMem`	—	—
`sdiff_erase` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike`	`Finset` `instSDiff` `erase` `instInsert`	—	—
`sdiff_erase_self` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike`	`Finset` `instSDiff` `erase` `instSingleton`	—	—
`sdiff_insert` 📖	mathematical	—	`Finset` `instSDiff` `instInsert` `erase`	—	—
`sdiff_insert_insert_of_mem_of_notMem` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike`	`Finset` `instInsert` `instSDiff`	—	—
`sdiff_singleton_eq_erase` 📖	mathematical	—	`Finset` `instSDiff` `instSingleton` `erase`	—	—
`sdiff_union_erase_cancel` 📖	mathematical	`Finset` `instHasSubset` `SetLike.instMembership` `instSetLike`	`Finset` `instUnion` `instSDiff` `erase`	—	—
`ssubset_iff_exists_subset_erase` 📖	mathematical	—	`Finset` `instHasSSubset` `SetLike.instMembership` `instSetLike` `instHasSubset` `erase`	—	—
`subset_insert_iff` 📖	mathematical	—	`Finset` `instHasSubset` `instInsert` `erase`	—	—
`subset_insert_iff_of_notMem` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike`	`Finset` `instHasSubset` `instInsert`	—	`subset_insert_iff` `erase_eq_of_notMem`
`subset_union_elim` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `Finset` `instSetLike` `Set.instUnion`	`Finset` `instUnion` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike` `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` `SetLike.instMembership` `instSetLike`	`Finset` `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.Nonempty` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.attach`	—	`Finset.attach_nonempty_iff`
`not_disjoint` 📖	mathematical	`Finset.Nonempty` `Finset` `Finset.instInter`	`Disjoint` `Finset` `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` `SetLike.instMembership` `Finset.instSetLike` `Finset.cons` `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