Commit 2023-01-16 08:13 5a1c5bb7

View on Github →

feat: port Data.Finset.Basic (#1555)

Estimated changes

Modified Mathlib/Data/Finset/Basic.lean

added theorem Directed.exists_mem_subset_of_finset_subset_bunionᵢ

added theorem DirectedOn.exists_mem_subset_of_finset_subset_bunionᵢ

added theorem Disjoint.forall_ne_finset

added def Equiv.sigmaEquivOptionOfInhabited

added theorem Finset.Insert.comm

added theorem Finset.Nonempty.bex

added theorem Finset.Nonempty.bunionᵢ

added theorem Finset.Nonempty.cons_induction

added theorem Finset.Nonempty.exists_eq_singleton_or_nontrivial

added theorem Finset.Nonempty.forall_const

added theorem Finset.Nonempty.mono

added theorem Finset.Nonempty.ne_empty

added theorem Finset.Nonempty.not_empty_toList

added theorem Finset.Nonempty.toList_ne_nil

added theorem Finset.Nonempty.to_subtype

added theorem Finset.Nonempty.to_type

added theorem Finset.Subset.antisymm

added theorem Finset.Subset.antisymm_iff

added theorem Finset.Subset.refl

added theorem Finset.Subset.trans

added theorem Finset.Superset.trans

added def Finset.attach

added theorem Finset.attach_empty

added theorem Finset.attach_eq_empty_iff

added theorem Finset.attach_nonempty_iff

added theorem Finset.attach_val

added theorem Finset.bind_toFinset

added theorem Finset.bot_eq_empty

added theorem Finset.bunionᵢ_bunionᵢ

added theorem Finset.bunionᵢ_congr

added theorem Finset.bunionᵢ_empty

added theorem Finset.bunionᵢ_filter_eq_of_maps_to

added theorem Finset.bunionᵢ_insert

added theorem Finset.bunionᵢ_inter

added theorem Finset.bunionᵢ_mono

added theorem Finset.bunionᵢ_nonempty

added theorem Finset.bunionᵢ_singleton_eq_self

added theorem Finset.bunionᵢ_subset

added theorem Finset.bunionᵢ_subset_bunionᵢ_of_subset_left

added theorem Finset.bunionᵢ_subset_iff_forall_subset

added theorem Finset.bunionᵢ_val

added def Finset.choose

added def Finset.chooseX

added theorem Finset.choose_mem

added theorem Finset.choose_property

added theorem Finset.choose_spec

added def Finset.coeEmb

added theorem Finset.coe_bunionᵢ

added theorem Finset.coe_coeEmb

added theorem Finset.coe_cons

added theorem Finset.coe_disjUnionᵢ

added theorem Finset.coe_empty

added theorem Finset.coe_eq_empty

added theorem Finset.coe_eq_pair

added theorem Finset.coe_eq_singleton

added theorem Finset.coe_erase

added theorem Finset.coe_filter

added theorem Finset.coe_inj

added theorem Finset.coe_injective

added theorem Finset.coe_insert

added theorem Finset.coe_inter

added theorem Finset.coe_mem

added theorem Finset.coe_nonempty

added theorem Finset.coe_pair

added theorem Finset.coe_range

added theorem Finset.coe_sdiff

added theorem Finset.coe_singleton

added theorem Finset.coe_sort_coe

added theorem Finset.coe_ssubset

added theorem Finset.coe_subset

added theorem Finset.coe_symmDiff

added theorem Finset.coe_toList

added theorem Finset.coe_union

added def Finset.cons

added theorem Finset.cons_eq_insert

added theorem Finset.cons_induction

added theorem Finset.cons_induction_on

added theorem Finset.cons_subset

added theorem Finset.cons_subset_cons

added theorem Finset.cons_val

added theorem Finset.dedup_eq_self

added def Finset.disjUnion

added theorem Finset.disjUnion_comm

added theorem Finset.disjUnion_empty

added theorem Finset.disjUnion_eq_union

added theorem Finset.disjUnion_singleton

added def Finset.disjUnionᵢ

added theorem Finset.disjUnionᵢ_cons

added theorem Finset.disjUnionᵢ_disjUnionᵢ

added theorem Finset.disjUnionᵢ_empty

added theorem Finset.disjUnionᵢ_eq_bunionᵢ

added theorem Finset.disjUnionᵢ_filter_eq_of_maps_to

added theorem Finset.disjUnionᵢ_val

added theorem Finset.disjoint_bunionᵢ_left

added theorem Finset.disjoint_bunionᵢ_right

added theorem Finset.disjoint_coe

added theorem Finset.disjoint_empty_left

added theorem Finset.disjoint_empty_right

added theorem Finset.disjoint_filter

added theorem Finset.disjoint_filter_filter'

added theorem Finset.disjoint_filter_filter

added theorem Finset.disjoint_filter_filter_neg

added theorem Finset.disjoint_iff_inter_eq_empty

added theorem Finset.disjoint_iff_ne

added theorem Finset.disjoint_insert_left

added theorem Finset.disjoint_insert_right

added theorem Finset.disjoint_left

added theorem Finset.disjoint_of_subset_left

added theorem Finset.disjoint_of_subset_right

added theorem Finset.disjoint_or_nonempty_inter

added theorem Finset.disjoint_right

added theorem Finset.disjoint_sdiff

added theorem Finset.disjoint_sdiff_inter

added theorem Finset.disjoint_self_iff_empty

added theorem Finset.disjoint_singleton

added theorem Finset.disjoint_singleton_left

added theorem Finset.disjoint_singleton_right

added theorem Finset.disjoint_union_left

added theorem Finset.disjoint_union_right

added theorem Finset.disjoint_val

added theorem Finset.empty_disjUnion

added theorem Finset.empty_inter

added theorem Finset.empty_sdiff

added theorem Finset.empty_ssubset

added theorem Finset.empty_ssubset_singleton

added theorem Finset.empty_subset

added theorem Finset.empty_toList

added theorem Finset.empty_union

added theorem Finset.empty_val

added theorem Finset.eq_empty_iff_forall_not_mem

added theorem Finset.eq_empty_of_forall_not_mem

added theorem Finset.eq_empty_of_isEmpty

added theorem Finset.eq_empty_of_ssubset_singleton

added theorem Finset.eq_empty_or_nonempty

added theorem Finset.eq_of_mem_of_not_mem_erase

added theorem Finset.eq_of_mem_singleton

added theorem Finset.eq_of_not_mem_of_mem_insert

added theorem Finset.eq_of_veq

added theorem Finset.eq_singleton_iff_nonempty_unique_mem

added theorem Finset.eq_singleton_iff_unique_mem

added theorem Finset.eq_singleton_or_nontrivial

added def Finset.erase

added theorem Finset.erase_bunionᵢ

added theorem Finset.erase_cons

added theorem Finset.erase_empty

added theorem Finset.erase_eq_empty_iff

added theorem Finset.erase_eq_of_not_mem

added theorem Finset.erase_eq_self

added theorem Finset.erase_idem

added theorem Finset.erase_inj

added theorem Finset.erase_injOn'

added theorem Finset.erase_injOn

added theorem Finset.erase_insert

added theorem Finset.erase_insert_eq_erase

added theorem Finset.erase_insert_of_ne

added theorem Finset.erase_insert_subset

added theorem Finset.erase_ne_self

added theorem Finset.erase_right_comm

added theorem Finset.erase_singleton

added theorem Finset.erase_ssubset

added theorem Finset.erase_ssubset_insert

added theorem Finset.erase_subset

added theorem Finset.erase_subset_erase

added theorem Finset.erase_subset_iff_of_mem

added theorem Finset.erase_val

added theorem Finset.exists_list_nodup_eq

added theorem Finset.exists_mem_empty_iff

added theorem Finset.exists_mem_insert

added theorem Finset.exists_of_ssubset

added theorem Finset.ext

added theorem Finset.ext_iff

added def Finset.filter

added theorem Finset.filter_and

added theorem Finset.filter_bunionᵢ

added theorem Finset.filter_congr

added theorem Finset.filter_cons

added theorem Finset.filter_cons_of_neg

added theorem Finset.filter_cons_of_pos

added theorem Finset.filter_disj_union

added theorem Finset.filter_empty

added theorem Finset.filter_eq'

added theorem Finset.filter_eq

added theorem Finset.filter_eq_empty_iff

added theorem Finset.filter_eq_self

added theorem Finset.filter_erase

added theorem Finset.filter_false

added theorem Finset.filter_false_of_mem

added theorem Finset.filter_filter

added theorem Finset.filter_insert

added theorem Finset.filter_inter

added theorem Finset.filter_inter_distrib

added theorem Finset.filter_inter_filter_neg_eq

added theorem Finset.filter_mem_eq_inter

added theorem Finset.filter_ne'

added theorem Finset.filter_ne

added theorem Finset.filter_nonempty_iff

added theorem Finset.filter_not

added theorem Finset.filter_or

added theorem Finset.filter_singleton

added theorem Finset.filter_ssubset

added theorem Finset.filter_subset

added theorem Finset.filter_subset_filter

added theorem Finset.filter_true

added theorem Finset.filter_true_of_mem

added theorem Finset.filter_union

added theorem Finset.filter_union_filter_neg_eq

added theorem Finset.filter_union_filter_of_codisjoint

added theorem Finset.filter_union_right

added theorem Finset.filter_val

added theorem Finset.forall_mem_cons

added theorem Finset.forall_mem_empty_iff

added theorem Finset.forall_mem_insert

added theorem Finset.forall_mem_union

added theorem Finset.induction_on'

added theorem Finset.induction_on_union

added theorem Finset.inf_eq_inter

added theorem Finset.insert_def

added theorem Finset.insert_eq

added theorem Finset.insert_eq_of_mem

added theorem Finset.insert_eq_self

added theorem Finset.insert_erase

added theorem Finset.insert_erase_subset

added theorem Finset.insert_idem

added theorem Finset.insert_inj

added theorem Finset.insert_inj_on

added theorem Finset.insert_inter_of_mem

added theorem Finset.insert_inter_of_not_mem

added theorem Finset.insert_ne_empty

added theorem Finset.insert_ne_self

added theorem Finset.insert_nonempty

added theorem Finset.insert_sdiff_insert

added theorem Finset.insert_sdiff_of_mem

added theorem Finset.insert_sdiff_of_not_mem

added theorem Finset.insert_subset

added theorem Finset.insert_subset_insert

added theorem Finset.insert_union

added theorem Finset.insert_union_distrib

added theorem Finset.insert_val'

added theorem Finset.insert_val

added theorem Finset.insert_val_of_not_mem

added theorem Finset.inter_assoc

added theorem Finset.inter_bunionᵢ

added theorem Finset.inter_comm

added theorem Finset.inter_congr_left

added theorem Finset.inter_congr_right

added theorem Finset.inter_distrib_left

added theorem Finset.inter_distrib_right

added theorem Finset.inter_empty

added theorem Finset.inter_eq_inter_iff_left

added theorem Finset.inter_eq_inter_iff_right

added theorem Finset.inter_eq_left_iff_subset

added theorem Finset.inter_eq_right_iff_subset

added theorem Finset.inter_filter

added theorem Finset.inter_insert_of_mem

added theorem Finset.inter_insert_of_not_mem

added theorem Finset.inter_inter_distrib_left

added theorem Finset.inter_inter_distrib_right

added theorem Finset.inter_inter_inter_comm

added theorem Finset.inter_left_comm

added theorem Finset.inter_left_idem

added theorem Finset.inter_right_comm

added theorem Finset.inter_right_idem

added theorem Finset.inter_sdiff

added theorem Finset.inter_sdiff_self

added theorem Finset.inter_self

added theorem Finset.inter_singleton_of_mem

added theorem Finset.inter_singleton_of_not_mem

added theorem Finset.inter_subset_inter

added theorem Finset.inter_subset_inter_left

added theorem Finset.inter_subset_inter_right

added theorem Finset.inter_subset_ite

added theorem Finset.inter_subset_left

added theorem Finset.inter_subset_right

added theorem Finset.inter_subset_union

added theorem Finset.inter_union_self

added theorem Finset.inter_val

added theorem Finset.inter_val_nd

added theorem Finset.isEmpty_coe_sort

added theorem Finset.ite_subset_union

added theorem Finset.le_eq_subset

added theorem Finset.le_iff_subset

added theorem Finset.le_piecewise_of_le_of_le

added theorem Finset.left_eq_union_iff_subset

added theorem Finset.lt_eq_subset

added theorem Finset.lt_iff_ssubset

added theorem Finset.mem_attach

added theorem Finset.mem_bunionᵢ

added theorem Finset.mem_coe

added theorem Finset.mem_cons

added theorem Finset.mem_cons_self

modified theorem Finset.mem_def

added theorem Finset.mem_disjUnion

added theorem Finset.mem_disjUnionᵢ

added theorem Finset.mem_erase

added theorem Finset.mem_erase_of_ne_of_mem

added theorem Finset.mem_filter

added theorem Finset.mem_insert

added theorem Finset.mem_insert_coe

added theorem Finset.mem_insert_of_mem

added theorem Finset.mem_insert_self

added theorem Finset.mem_inter

added theorem Finset.mem_inter_of_mem

added theorem Finset.mem_mk

added theorem Finset.mem_of_mem_erase

added theorem Finset.mem_of_mem_filter

added theorem Finset.mem_of_mem_insert_of_ne

added theorem Finset.mem_of_mem_inter_left

added theorem Finset.mem_of_mem_inter_right

added theorem Finset.mem_of_subset

added theorem Finset.mem_range

added theorem Finset.mem_range_le

added theorem Finset.mem_range_sub_ne_zero

added theorem Finset.mem_range_succ_iff

added theorem Finset.mem_sdiff

added theorem Finset.mem_singleton

added theorem Finset.mem_singleton_self

added theorem Finset.mem_symmDiff

added theorem Finset.mem_toList

added theorem Finset.mem_union

added theorem Finset.mem_union_left

added theorem Finset.mem_union_right

added theorem Finset.mem_val

added theorem Finset.mk_coe

added theorem Finset.mk_cons

added theorem Finset.mk_zero

added theorem Finset.monotone_filter_left

added theorem Finset.monotone_filter_right

added theorem Finset.ne_empty_of_mem

added theorem Finset.ne_insert_of_not_mem

added theorem Finset.ne_of_mem_erase

added theorem Finset.nodup_toList

added theorem Finset.nonempty_coe_sort

added theorem Finset.nonempty_cons

added theorem Finset.nonempty_iff_eq_singleton_default

added theorem Finset.nonempty_iff_ne_empty

added theorem Finset.nonempty_mk

added theorem Finset.nonempty_of_ne_empty

added theorem Finset.nonempty_range_iff

added theorem Finset.nonempty_range_succ

added theorem Finset.not_disjoint_iff

added theorem Finset.not_disjoint_iff_nonempty_inter

added theorem Finset.not_mem_empty

added theorem Finset.not_mem_erase

added theorem Finset.not_mem_mono

added theorem Finset.not_mem_range_self

added theorem Finset.not_mem_sdiff_of_mem_right

added theorem Finset.not_mem_sdiff_of_not_mem_left

added theorem Finset.not_mem_singleton

added theorem Finset.not_mem_union

added theorem Finset.not_nonempty_empty

added theorem Finset.not_nonempty_iff_eq_empty

added theorem Finset.not_ssubset_empty

added theorem Finset.not_subset

added theorem Finset.pair_comm

added theorem Finset.pair_eq_singleton

added theorem Finset.pairwiseDisjoint_coe

added theorem Finset.pairwise_cons'

added theorem Finset.pairwise_cons

added theorem Finset.pairwise_subtype_iff_pairwise_finset'

added theorem Finset.pairwise_subtype_iff_pairwise_finset

added def Finset.piecewise

added theorem Finset.piecewise_cases

added theorem Finset.piecewise_coe

added theorem Finset.piecewise_congr

added theorem Finset.piecewise_empty

added theorem Finset.piecewise_eq_of_mem

added theorem Finset.piecewise_eq_of_not_mem

added theorem Finset.piecewise_idem_left

added theorem Finset.piecewise_idem_right

added theorem Finset.piecewise_insert

added theorem Finset.piecewise_insert_of_ne

added theorem Finset.piecewise_insert_self

added theorem Finset.piecewise_le_of_le_of_le

added theorem Finset.piecewise_le_piecewise'

added theorem Finset.piecewise_le_piecewise

added theorem Finset.piecewise_mem_Icc'

added theorem Finset.piecewise_mem_Icc

added theorem Finset.piecewise_mem_Icc_of_mem_of_mem

added theorem Finset.piecewise_mem_set_pi

added theorem Finset.piecewise_piecewise_of_subset_left

added theorem Finset.piecewise_piecewise_of_subset_right

added theorem Finset.piecewise_singleton

added def Finset.range

added theorem Finset.range_add_one

added theorem Finset.range_eq_empty_iff

added theorem Finset.range_filter_eq

added theorem Finset.range_mono

added theorem Finset.range_one

added theorem Finset.range_subset

added theorem Finset.range_succ

added theorem Finset.range_val

added theorem Finset.range_zero

added theorem Finset.right_eq_union_iff_subset

added theorem Finset.sdiff_disjoint

added theorem Finset.sdiff_empty

added theorem Finset.sdiff_eq_empty_iff_subset

added theorem Finset.sdiff_eq_filter

added theorem Finset.sdiff_eq_sdiff_iff_inter_eq_inter

added theorem Finset.sdiff_eq_self

added theorem Finset.sdiff_eq_self_iff_disjoint

added theorem Finset.sdiff_eq_self_of_disjoint

added theorem Finset.sdiff_erase

added theorem Finset.sdiff_idem

added theorem Finset.sdiff_insert

added theorem Finset.sdiff_insert_insert_of_mem_of_not_mem

added theorem Finset.sdiff_insert_of_not_mem

added theorem Finset.sdiff_inter_distrib_right

added theorem Finset.sdiff_inter_self

added theorem Finset.sdiff_inter_self_left

added theorem Finset.sdiff_inter_self_right

added theorem Finset.sdiff_nonempty

added theorem Finset.sdiff_sdiff_eq_self

added theorem Finset.sdiff_sdiff_left'

added theorem Finset.sdiff_sdiff_self_left

added theorem Finset.sdiff_self

added theorem Finset.sdiff_singleton_eq_erase

added theorem Finset.sdiff_singleton_not_mem_eq_self

added theorem Finset.sdiff_ssubset

added theorem Finset.sdiff_subset

added theorem Finset.sdiff_subset_sdiff

added theorem Finset.sdiff_union_distrib

added theorem Finset.sdiff_union_inter

added theorem Finset.sdiff_union_of_subset

added theorem Finset.sdiff_union_self_eq_union

added theorem Finset.sdiff_val

added theorem Finset.self_mem_range_succ

added theorem Finset.setOf_mem

added theorem Finset.singleton_bunionᵢ

added theorem Finset.singleton_disjUnion

added theorem Finset.singleton_disjUnionᵢ

added theorem Finset.singleton_iff_unique_mem

added theorem Finset.singleton_inj

added theorem Finset.singleton_injective

added theorem Finset.singleton_inter_of_mem

added theorem Finset.singleton_inter_of_not_mem

added theorem Finset.singleton_ne_empty

added theorem Finset.singleton_nonempty

added theorem Finset.singleton_subset_iff

added theorem Finset.singleton_subset_set_iff

added theorem Finset.singleton_subset_singleton

added theorem Finset.singleton_val

added theorem Finset.sizeOf_lt_sizeOf_of_mem

added theorem Finset.ssubset_cons

added theorem Finset.ssubset_def

added theorem Finset.ssubset_iff

added theorem Finset.ssubset_iff_exists_cons_subset

added theorem Finset.ssubset_iff_exists_subset_erase

added theorem Finset.ssubset_iff_of_subset

added theorem Finset.ssubset_iff_subset_ne

added theorem Finset.ssubset_insert

added theorem Finset.ssubset_of_ssubset_of_subset

added theorem Finset.ssubset_of_subset_of_ssubset

added theorem Finset.ssubset_singleton_iff

added theorem Finset.subset_bunionᵢ_of_mem

added theorem Finset.subset_coe_filter_of_subset_forall

added theorem Finset.subset_cons

added theorem Finset.subset_def

added theorem Finset.subset_empty

added theorem Finset.subset_erase

added theorem Finset.subset_iff

added theorem Finset.subset_insert

added theorem Finset.subset_insert_iff

added theorem Finset.subset_insert_iff_of_not_mem

added theorem Finset.subset_inter

added theorem Finset.subset_inter_iff

added theorem Finset.subset_sdiff

added theorem Finset.subset_singleton_iff'

added theorem Finset.subset_singleton_iff

added theorem Finset.subset_union_elim

added theorem Finset.subset_union_left

added theorem Finset.subset_union_right

added def Finset.subtypeInsertEquivOption

added theorem Finset.sup_eq_union

added theorem Finset.toList_cons

added theorem Finset.toList_empty

added theorem Finset.toList_eq_nil

added theorem Finset.toList_insert

added theorem Finset.toList_toFinset

added def Finset.toSet

added theorem Finset.union_assoc

added theorem Finset.union_comm

added theorem Finset.union_congr_left

added theorem Finset.union_congr_right

added theorem Finset.union_distrib_left

added theorem Finset.union_distrib_right

added theorem Finset.union_empty

added theorem Finset.union_eq_empty_iff

added theorem Finset.union_eq_left_iff_subset

added theorem Finset.union_eq_right_iff_subset

added theorem Finset.union_eq_sdiff_union_sdiff_union_inter

added theorem Finset.union_eq_union_iff_left

added theorem Finset.union_eq_union_iff_right

added theorem Finset.union_idempotent

added theorem Finset.union_insert

added theorem Finset.union_inter_cancel_left

added theorem Finset.union_inter_cancel_right

added theorem Finset.union_left_comm

added theorem Finset.union_left_idem

added theorem Finset.union_right_comm

added theorem Finset.union_right_idem

added theorem Finset.union_sdiff_distrib

added theorem Finset.union_sdiff_left

added theorem Finset.union_sdiff_of_subset

added theorem Finset.union_sdiff_right

added theorem Finset.union_sdiff_self

added theorem Finset.union_sdiff_self_eq_union

added theorem Finset.union_sdiff_symm

added theorem Finset.union_self

added theorem Finset.union_subset

added theorem Finset.union_subset_iff

added theorem Finset.union_subset_left

added theorem Finset.union_subset_right

added theorem Finset.union_subset_union

added theorem Finset.union_union_distrib_left

added theorem Finset.union_union_distrib_right

added theorem Finset.union_union_union_comm

added theorem Finset.union_val

added theorem Finset.union_val_nd

added theorem Finset.update_eq_piecewise

added theorem Finset.update_piecewise

added theorem Finset.update_piecewise_of_mem

added theorem Finset.update_piecewise_of_not_mem

added theorem Finset.val_eq_zero

added theorem Finset.val_inj

added theorem Finset.val_injective

added theorem Finset.val_le_iff

added theorem Finset.val_le_iff_val_subset

added theorem Finset.val_lt_iff

added theorem Finset.val_toFinset

added theorem List.coe_toFinset

added theorem List.disjoint_toFinset_iff_disjoint

added theorem List.mem_toFinset

added theorem List.perm_of_nodup_nodup_toFinset_eq

added theorem List.toFinset.ext

added theorem List.toFinset.ext_iff

added def List.toFinset

added theorem List.toFinset_append

added theorem List.toFinset_coe

added theorem List.toFinset_cons

added theorem List.toFinset_eq

added theorem List.toFinset_eq_empty_iff

added theorem List.toFinset_eq_iff_perm_dedup

added theorem List.toFinset_eq_of_perm

added theorem List.toFinset_inter

added theorem List.toFinset_nil

added theorem List.toFinset_replicate_of_ne_zero

added theorem List.toFinset_reverse

added theorem List.toFinset_surj_on

added theorem List.toFinset_surjective

added theorem List.toFinset_union

added theorem List.toFinset_val

added theorem Multiset.Nodup.toFinset_inj

added theorem Multiset.disjoint_toFinset

added theorem Multiset.mem_toFinset

added def Multiset.toFinset

added theorem Multiset.toFinset_add

added theorem Multiset.toFinset_bind_dedup

added theorem Multiset.toFinset_cons

added theorem Multiset.toFinset_dedup

added theorem Multiset.toFinset_eq

added theorem Multiset.toFinset_eq_empty

added theorem Multiset.toFinset_inter

added theorem Multiset.toFinset_nsmul

added theorem Multiset.toFinset_singleton

added theorem Multiset.toFinset_ssubset

added theorem Multiset.toFinset_subset

added theorem Multiset.toFinset_union

added theorem Multiset.toFinset_val

added theorem Multiset.toFinset_zero

added theorem coe_notMemRangeEquiv

added theorem coe_notMemRangeEquiv_symm

added def notMemRangeEquiv