Commit 2025-02-09 06:38 0868356d

View on Github →

chore(Data/Set/Basic): split insert / singleton / pair to new file (#21567) This PR splits insert singleton and pair lemmas off of Data.Set.Basic, mitigating an instance of a long file, and bringing the directory structure more in line with Finset

Estimated changes

deleted theorem Prop.compl_singleton
deleted theorem Set.Nonempty.eq_one
deleted theorem Set.Nonempty.eq_zero
deleted theorem Set.compl_ne_eq_singleton
deleted theorem Set.compl_singleton_eq
deleted theorem Set.default_coe_singleton
deleted theorem Set.disjoint_singleton
deleted theorem Set.eq_of_mem_singleton
deleted theorem Set.exists_mem_insert
deleted theorem Set.forall_mem_insert
deleted theorem Set.insert_comm
deleted theorem Set.insert_def
deleted theorem Set.insert_diff_of_mem
deleted theorem Set.insert_diff_singleton
deleted theorem Set.insert_eq
deleted theorem Set.insert_eq_of_mem
deleted theorem Set.insert_eq_self
deleted theorem Set.insert_erase_invOn
deleted theorem Set.insert_idem
deleted theorem Set.insert_inj
deleted theorem Set.insert_inter_distrib
deleted theorem Set.insert_inter_of_mem
deleted theorem Set.insert_ne_self
deleted theorem Set.insert_nonempty
deleted theorem Set.insert_subset
deleted theorem Set.insert_subset_iff
deleted theorem Set.insert_subset_insert
deleted theorem Set.insert_union
deleted theorem Set.insert_union_distrib
deleted theorem Set.inter_insert_of_mem
deleted theorem Set.mem_diff_singleton
deleted theorem Set.mem_insert
deleted theorem Set.mem_insert_iff
deleted theorem Set.mem_insert_of_mem
deleted theorem Set.mem_singleton
deleted theorem Set.mem_singleton_iff
deleted theorem Set.mem_singleton_of_eq
deleted theorem Set.ne_insert_of_not_mem
deleted theorem Set.nmem_singleton_empty
deleted theorem Set.not_mem_singleton_iff
deleted theorem Set.pair_comm
deleted theorem Set.pair_diff_left
deleted theorem Set.pair_diff_right
deleted theorem Set.pair_eq_pair_iff
deleted theorem Set.pair_eq_singleton
deleted theorem Set.pair_subset
deleted theorem Set.pair_subset_iff
deleted theorem Set.powerset_singleton
deleted theorem Set.setOf_eq_eq_singleton
deleted theorem Set.singleton_def
deleted theorem Set.singleton_injective
deleted theorem Set.singleton_ne_empty
deleted theorem Set.singleton_nonempty
deleted theorem Set.singleton_subset_iff
deleted theorem Set.singleton_union
deleted theorem Set.ssubset_iff_insert
deleted theorem Set.ssubset_insert
deleted theorem Set.ssubset_singleton_iff
deleted theorem Set.subset_diff_singleton
deleted theorem Set.subset_insert
deleted theorem Set.subset_insert_iff
deleted theorem Set.subset_pair_iff
deleted theorem Set.subset_pair_iff_eq
deleted theorem Set.subset_singleton_iff
deleted theorem Set.union_insert
deleted theorem Set.union_singleton
added theorem Prop.compl_singleton
added theorem Set.Nonempty.eq_one
added theorem Set.Nonempty.eq_zero
added theorem Set.compl_singleton_eq
added theorem Set.disjoint_singleton
added theorem Set.exists_mem_insert
added theorem Set.forall_mem_insert
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_erase_invOn
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_subset_iff
added theorem Set.insert_union
added theorem Set.mem_diff_singleton
added theorem Set.mem_insert
added theorem Set.mem_insert_iff
added theorem Set.mem_insert_of_mem
added theorem Set.mem_singleton
added theorem Set.mem_singleton_iff
added theorem Set.pair_comm
added theorem Set.pair_diff_left
added theorem Set.pair_diff_right
added theorem Set.pair_eq_pair_iff
added theorem Set.pair_eq_singleton
added theorem Set.pair_subset
added theorem Set.pair_subset_iff
added theorem Set.powerset_singleton
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_iff_insert
added theorem Set.ssubset_insert
added theorem Set.subset_insert
added theorem Set.subset_insert_iff
added theorem Set.subset_pair_iff
added theorem Set.subset_pair_iff_eq
added theorem Set.union_insert
added theorem Set.union_singleton