Commit 2023-01-11 08:02 ca98f897

View on Github →

feat: A set is either a subsingleton or nontrivial (#1047) Match https://github.com/leanprover-community/mathlib/pull/17901 and https://github.com/leanprover-community/mathlib/pull/17957

Estimated changes

deleted theorem Disjoint.ne_of_mem
deleted theorem Set.diff_eq_self
deleted theorem Set.disjoint_diff
modified theorem Set.disjoint_empty
modified theorem Set.disjoint_iff_forall_ne
modified theorem Set.disjoint_of_subset
modified theorem Set.disjoint_of_subset_left
modified theorem Set.disjoint_right
modified theorem Set.disjoint_singleton
modified theorem Set.disjoint_singleton_left
modified theorem Set.disjoint_union_left
modified theorem Set.disjoint_union_right
modified theorem Set.disjoint_univ
modified theorem Set.empty_disjoint
modified theorem Set.not_disjoint_iff
modified theorem Set.subset_diff
modified theorem Set.univ_disjoint
modified theorem Set.interᵢ_congr
modified theorem Set.interᵢ_const
added theorem Set.interᵢ_eq_const
modified theorem Set.interᵢ₂_congr
modified theorem Set.unionᵢ_congr
modified theorem Set.unionᵢ_const
added theorem Set.unionᵢ_eq_const
modified theorem Set.unionᵢ₂_congr
added theorem le_sdiff
added theorem sdiff_eq_left
deleted theorem Codisjoint.comm
added theorem Codisjoint_comm
deleted theorem Disjoint.comm
added theorem disjoint_comm
modified theorem ne_of_not_subset
modified theorem ne_of_not_superset
modified theorem ne_of_ssubset
modified theorem ne_of_ssuperset
modified theorem ssubset_asymm
modified theorem ssubset_irrefl
modified theorem ssubset_irrfl
modified theorem ssubset_trans
modified theorem subset_antisymm
modified theorem subset_of_eq
added theorem subset_of_eq_of_subset
added theorem subset_of_subset_of_eq
modified theorem subset_refl
modified theorem subset_rfl
modified theorem subset_trans
modified theorem superset_antisymm
modified theorem superset_of_eq