feat(Data/Set): add Set.Uncountable

Mathlib/Analysis/Real/Cardinality.lean

@@ -268,23 +268,23 @@ lemma Real.Ioo_countable_iff {x y : ℝ} :
     (Ioo x y).Countable ↔ y ≤ x := by
   refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
   contrapose! h
-  rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioo_real h, not_le]
+  rw [← Cardinal.aleph0_lt_iff_set_uncountable, Cardinal.mk_Ioo_real h]
   exact Cardinal.aleph0_lt_continuum
 
 @[simp]
 lemma Real.Ico_countable_iff {x y : ℝ} :
     (Ico x y).Countable ↔ y ≤ x := by
   refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
   contrapose! h
-  rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ico_real h, not_le]
+  rw [← Cardinal.aleph0_lt_iff_set_uncountable, Cardinal.mk_Ico_real h]
   exact Cardinal.aleph0_lt_continuum
 
 @[simp]
 lemma Real.Ioc_countable_iff {x y : ℝ} :
     (Ioc x y).Countable ↔ y ≤ x := by
   refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
   contrapose! h
-  rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioc_real h, not_le]
+  rw [← Cardinal.aleph0_lt_iff_set_uncountable, Cardinal.mk_Ioc_real h]
   exact Cardinal.aleph0_lt_continuum
 
 @[simp]
@@ -295,7 +295,7 @@ lemma Real.Icc_countable_iff {x y : ℝ} :
     · simp [heq]
     · simp [hlt]⟩
   contrapose! h
-  rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Icc_real h, not_le]
+  rw [← Cardinal.aleph0_lt_iff_set_uncountable, Cardinal.mk_Icc_real h]
   exact Cardinal.aleph0_lt_continuum
 
 end Cardinal

Mathlib/Data/Set/Countable.lean

@@ -330,3 +330,76 @@ end Set
 
 theorem Finset.countable_toSet (s : Finset α) : Set.Countable (↑s : Set α) :=
   s.finite_toSet.countable
+
+namespace Set
+
+/-- A set is uncountable if it is not countable.
+
+This is protected so that it does not conflict with global `Uncountable`. -/
+protected def Uncountable (s : Set α) : Prop :=
+  ¬s.Countable
+
+@[simp, push]
+theorem not_countable_iff_uncountable {s : Set α} : ¬s.Countable ↔ s.Uncountable := .rfl
+
+@[simp, push]
+theorem not_uncountable_iff_countable {s : Set α} : ¬s.Uncountable ↔ s.Countable :=
+  not_not
+
+alias ⟨_, Countable.not_uncountable⟩ := not_uncountable_iff_countable
+
+@[simp] lemma Uncountable.not_countable {s : Set α} (hs : s.Uncountable) : ¬ s.Countable := hs
+
+attribute [simp] Countable.not_uncountable
+
+theorem uncountable_coe_iff {s : Set α} : Uncountable s ↔ s.Uncountable :=
+  not_countable_iff.symm.trans countable_coe_iff.not
+
+alias ⟨_root_.Uncountable.to_set, Uncountable.to_subtype⟩ := uncountable_coe_iff
+
+theorem uncountable_univ_iff : (@univ α).Uncountable ↔ Uncountable α := by
+  rw [Set.Uncountable, countable_univ_iff, not_countable_iff]
+
+theorem uncountable_univ [h : Uncountable α] : (@univ α).Uncountable :=
+  uncountable_univ_iff.2 h
+
+protected lemma Uncountable.mono {s t : Set α} (h : s ⊆ t) : s.Uncountable → t.Uncountable :=
+  mt (·.mono h)
+
+theorem uncountable_of_countable_compl [Uncountable α] {s : Set α} (hs : sᶜ.Countable) :
+    s.Uncountable := fun h =>
+  Set.uncountable_univ (α := α) (by simpa using hs.union h)
+
+theorem Countable.uncountable_compl [Uncountable α] {s : Set α} (hs : s.Countable) :
+    sᶜ.Uncountable := fun h =>
+  Set.uncountable_univ (α := α) (by simpa using hs.union h)
+
+theorem Uncountable.diff {s t : Set α} (hs : s.Uncountable) (ht : t.Countable) :
+    (s \ t).Uncountable := fun h =>
+  hs <| h.of_diff ht
+
+@[simp]
+theorem uncountable_union {s t : Set α} : (s ∪ t).Uncountable ↔ s.Uncountable ∨ t.Uncountable := by
+  simp only [Set.Uncountable, countable_union, not_and_or]
+
+theorem Uncountable.of_image (f : α → β) {s : Set α} (hs : (f '' s).Uncountable) : s.Uncountable :=
+  mt (Countable.image · f) hs
+
+theorem Uncountable.image {s : Set α} {f : α → β} (hs : s.Uncountable) (hi : InjOn f s) :
+    (f '' s).Uncountable :=
+  mt (countable_of_injective_of_countable_image hi) hs
+
+theorem Uncountable.range [Uncountable α] {f : α → β} (hi : Injective f) :
+    (range f).Uncountable := by
+  simpa using uncountable_univ.image (hi.injOn (s := Set.univ))
+
+theorem Uncountable.infinite {s : Set α} (hs : s.Uncountable) : s.Infinite :=
+  mt Finite.countable hs
+
+theorem Uncountable.nonempty {s : Set α} (hs : s.Uncountable) : s.Nonempty :=
+  hs.infinite.nonempty
+
+theorem Uncountable.nontrivial {s : Set α} (hs : s.Uncountable) : s.Nontrivial :=
+  hs.infinite.nontrivial
+
+end Set

Mathlib/SetTheory/Cardinal/Basic.lean

@@ -451,6 +451,11 @@ theorem aleph0_lt_mk_iff : ℵ₀ < #α ↔ Uncountable α := by
 theorem aleph0_lt_mk [Uncountable α] : ℵ₀ < #α :=
   aleph0_lt_mk_iff.mpr ‹_›
 
+theorem aleph0_lt_iff_set_uncountable {s : Set α} : ℵ₀ < #s ↔ s.Uncountable :=
+  aleph0_lt_mk_iff.trans uncountable_coe_iff
+
+alias ⟨_, _root_.Set.Uncountable.aleph0_lt⟩ := aleph0_lt_iff_set_uncountable
+
 instance canLiftCardinalNat : CanLift Cardinal ℕ (↑) fun x => x < ℵ₀ :=
   ⟨fun _ hx =>
     let ⟨n, hn⟩ := lt_aleph0.mp hx