Commit 2022-12-12 01:34 f1dedcd9

View on Github →

feat: port Data.Set.Basic (#892) 1b36dabc50929b36caec16306358a5cc44ab441e If more PRs arrive in mathlib that slice up Data.Set.Basic, that's okay, we'll just delete the relevant sections here. TODO: finish linting

Estimated changes

added theorem Disjoint.inter_eq
added theorem Eq.subset
added theorem Membership.Mem.out
added def Set.Elem
added theorem Set.MemUnion.elim
added theorem Set.Nonempty.eq_univ
added theorem Set.Nonempty.inl
added theorem Set.Nonempty.inr
added theorem Set.Nonempty.left
added theorem Set.Nonempty.mono
added theorem Set.Nonempty.of_diff
added theorem Set.Nonempty.right
added theorem Set.Nonempty.to_type
added theorem Set.Nontrivial.mono
added theorem Set.Subset.antisymm
added theorem Set.Subset.refl
added theorem Set.Subset.rfl
added theorem Set.Subset.trans
added theorem Set.Subsingleton.anti
added theorem Set.ball_empty_iff
added theorem Set.ball_insert_iff
added theorem Set.bex_insert_iff
added theorem Set.bot_eq_empty
added theorem Set.coe_eq_subtype
added theorem Set.coe_inclusion
added theorem Set.coe_setOf
added theorem Set.compl_def
added theorem Set.compl_empty
added theorem Set.compl_empty_iff
added theorem Set.compl_eq_univ_diff
added theorem Set.compl_inter
added theorem Set.compl_inter_self
added theorem Set.compl_ne_univ
added theorem Set.compl_setOf
added theorem Set.compl_singleton_eq
added theorem Set.compl_subset_comm
added theorem Set.compl_subset_compl
added theorem Set.compl_union
added theorem Set.compl_union_self
added theorem Set.compl_univ
added theorem Set.compl_univ_iff
added theorem Set.diff_compl
added theorem Set.diff_diff
added theorem Set.diff_diff_comm
added theorem Set.diff_diff_right
added theorem Set.diff_empty
added theorem Set.diff_eq
added theorem Set.diff_eq_empty
added theorem Set.diff_eq_self
added theorem Set.diff_inter
added theorem Set.diff_inter_diff
added theorem Set.diff_inter_self
added theorem Set.diff_self
added theorem Set.diff_self_inter
added theorem Set.diff_subset
added theorem Set.diff_subset_comm
added theorem Set.diff_subset_diff
added theorem Set.diff_subset_iff
added theorem Set.diff_union_inter
added theorem Set.diff_union_self
added theorem Set.diff_univ
added theorem Set.disjoint_left
added theorem Set.disjoint_right
added theorem Set.empty_def
added theorem Set.empty_diff
added theorem Set.empty_inter
added theorem Set.empty_ne_univ
added theorem Set.empty_ssubset
added theorem Set.empty_subset
added theorem Set.empty_union
added theorem Set.eq_univ_iff_forall
added theorem Set.eq_univ_of_forall
added theorem Set.eq_univ_of_subset
added theorem Set.exists_of_ssubset
added theorem Set.ext_iff
added theorem Set.forall_in_swap
added def Set.inclusion
added theorem Set.inclusion_eq_id
added theorem Set.inclusion_mk
added theorem Set.inclusion_right
added theorem Set.inclusion_self
added theorem Set.inf_eq_inter
added theorem Set.insert_comm
added theorem Set.insert_def
added theorem Set.insert_diff_of_mem
added theorem Set.insert_eq
added theorem Set.insert_eq_of_mem
added theorem Set.insert_eq_self
added theorem Set.insert_idem
added theorem Set.insert_inj
added theorem Set.insert_ne_self
added theorem Set.insert_nonempty
added theorem Set.insert_subset
added theorem Set.insert_union
added theorem Set.inter_assoc
added theorem Set.inter_comm
added theorem Set.inter_compl_self
added theorem Set.inter_congr_left
added theorem Set.inter_congr_right
added theorem Set.inter_def
added theorem Set.inter_diff_assoc
added theorem Set.inter_diff_self
added theorem Set.inter_distrib_left
added theorem Set.inter_empty
added theorem Set.inter_left_comm
added theorem Set.inter_nonempty
added theorem Set.inter_right_comm
added theorem Set.inter_self
added theorem Set.inter_subset
added theorem Set.inter_subset_inter
added theorem Set.inter_subset_ite
added theorem Set.inter_subset_left
added theorem Set.inter_subset_right
added theorem Set.inter_union_compl
added theorem Set.inter_union_diff
added theorem Set.inter_univ
added theorem Set.isEmpty_coe_sort
added theorem Set.ite_compl
added theorem Set.ite_diff_self
added theorem Set.ite_empty
added theorem Set.ite_empty_left
added theorem Set.ite_empty_right
added theorem Set.ite_inter
added theorem Set.ite_inter_inter
added theorem Set.ite_inter_self
added theorem Set.ite_left
added theorem Set.ite_mono
added theorem Set.ite_right
added theorem Set.ite_same
added theorem Set.ite_subset_union
added theorem Set.ite_univ
added theorem Set.le_eq_subset
added theorem Set.le_iff_subset
added theorem Set.lt_eq_ssubset
added theorem Set.lt_iff_ssubset
added theorem Set.mem_compl
added theorem Set.mem_compl_iff
added theorem Set.mem_def
added theorem Set.mem_diff
added theorem Set.mem_diff_of_mem
added theorem Set.mem_diff_singleton
added theorem Set.mem_dite
added theorem Set.mem_dite_univ_left
added theorem Set.mem_insert
added theorem Set.mem_insert_iff
added theorem Set.mem_insert_of_mem
added theorem Set.mem_inter
added theorem Set.mem_inter_iff
added theorem Set.mem_ite_empty_left
added theorem Set.mem_ite_univ_left
added theorem Set.mem_ite_univ_right
added theorem Set.mem_of_eq_of_mem
added theorem Set.mem_of_mem_diff
added theorem Set.mem_powerset
added theorem Set.mem_powerset_iff
added theorem Set.mem_sep
added theorem Set.mem_sep_iff
added theorem Set.mem_setOf
added theorem Set.mem_singleton
added theorem Set.mem_singleton_iff
added theorem Set.mem_symmDiff
added theorem Set.mem_union
added theorem Set.mem_union_left
added theorem Set.mem_union_right
added theorem Set.mem_univ
added theorem Set.monotone_powerset
added theorem Set.nmem_setOf_iff
added theorem Set.nonempty_coe_sort
added theorem Set.nonempty_compl
added theorem Set.nonempty_def
added theorem Set.nonempty_diff
added theorem Set.nonempty_of_mem
added theorem Set.nontrivial_mono
added theorem Set.nontrivial_of_lt
added theorem Set.nontrivial_pair
added theorem Set.nontrivial_univ
added theorem Set.not_mem_compl_iff
added theorem Set.not_mem_empty
added theorem Set.not_mem_subset
added theorem Set.not_nonempty_empty
added theorem Set.not_nontrivial_iff
added theorem Set.not_not_mem
added theorem Set.not_subset
added theorem Set.pair_comm
added theorem Set.pair_eq_pair_iff
added theorem Set.pair_eq_singleton
added theorem Set.powerset_empty
added theorem Set.powerset_inter
added theorem Set.powerset_mono
added theorem Set.powerset_nonempty
added theorem Set.powerset_univ
added theorem Set.sep_and
added theorem Set.sep_empty
added theorem Set.sep_eq_of_subset
added theorem Set.sep_ext_iff
added theorem Set.sep_false
added theorem Set.sep_inter
added theorem Set.sep_mem_eq
added theorem Set.sep_or
added theorem Set.sep_setOf
added theorem Set.sep_subset
added theorem Set.sep_true
added theorem Set.sep_union
added theorem Set.sep_univ
added theorem Set.setOf_and
added theorem Set.setOf_app_iff
added theorem Set.setOf_bijective
added theorem Set.setOf_false
added theorem Set.setOf_mem_eq
added theorem Set.setOf_or
added theorem Set.setOf_set
added theorem Set.setOf_subset_setOf
added theorem Set.setOf_true
added theorem Set.singleton_def
added theorem Set.singleton_ne_empty
added theorem Set.singleton_nonempty
added theorem Set.singleton_union
added theorem Set.ssubset_def
added theorem Set.ssubset_iff_insert
added theorem Set.ssubset_insert
added theorem Set.ssubset_univ_iff
added theorem Set.subset_compl_comm
added theorem Set.subset_def
added theorem Set.subset_diff_union
added theorem Set.subset_empty_iff
added theorem Set.subset_eq_empty
added theorem Set.subset_insert
added theorem Set.subset_inter
added theorem Set.subset_inter_iff
added theorem Set.subset_ite
added theorem Set.subset_union_left
added theorem Set.subset_union_right
added theorem Set.subset_univ
added theorem Set.subsingleton_coe
added theorem Set.subsingleton_empty
added theorem Set.subsingleton_isBot
added theorem Set.subsingleton_isTop
added theorem Set.subsingleton_univ
added theorem Set.sup_eq_union
added theorem Set.symmDiff_eq_empty
added theorem Set.symmDiff_nonempty
added theorem Set.top_eq_univ
added theorem Set.union_assoc
added theorem Set.union_comm
added theorem Set.union_compl_self
added theorem Set.union_congr_left
added theorem Set.union_congr_right
added theorem Set.union_def
added theorem Set.union_diff_cancel'
added theorem Set.union_diff_cancel
added theorem Set.union_diff_distrib
added theorem Set.union_diff_left
added theorem Set.union_diff_right
added theorem Set.union_diff_self
added theorem Set.union_distrib_left
added theorem Set.union_empty
added theorem Set.union_empty_iff
added theorem Set.union_insert
added theorem Set.union_left_comm
added theorem Set.union_nonempty
added theorem Set.union_right_comm
added theorem Set.union_self
added theorem Set.union_singleton
added theorem Set.union_subset
added theorem Set.union_subset_iff
added theorem Set.union_subset_union
added theorem Set.union_univ
added theorem Set.univ_eq_empty_iff
added theorem Set.univ_eq_true_false
added theorem Set.univ_inter
added theorem Set.univ_nonempty
added theorem Set.univ_subset_iff
added theorem Set.univ_union
added theorem Set.univ_unique
added theorem SetCoe.exists'
added theorem SetCoe.exists
added theorem SetCoe.ext
added theorem SetCoe.ext_iff
added theorem SetCoe.forall'
added theorem SetCoe.forall
added theorem Subsingleton.set_cases
added theorem Subtype.mem
added theorem set_coe_cast