@[simp]

theorem Cardinal.aleph0_le_mk_set {α : Type u_1} {s : Set α} : aleph0 ≤ mk ↑s ↔ s.Infinite

@[simp]

theorem Cardinal.mk_diff_eq_left' {α : Type u_1} {s t : Set α} (hs : s.Infinite) (hst : mk ↑(s ∩ t) < mk ↑s) : mk ↑(s \ t) = mk ↑s

@[simp]

theorem Cardinal.mk_diff_eq_left {α : Type u_1} {s t : Set α} (hs : s.Infinite) (hts : mk ↑t < mk ↑s) : mk ↑(s \ t) = mk ↑s

@[simp]

theorem Cardinal.mk_diff_eq_left_of_finite' {α : Type u_1} {s t : Set α} (hs : s.Infinite) (hst : (s ∩ t).Finite) : mk ↑(s \ t) = mk ↑s

@[simp]

theorem Cardinal.mk_diff_eq_left_of_finite {α : Type u_1} {s t : Set α} (hs : s.Infinite) (ht : t.Finite) : mk ↑(s \ t) = mk ↑s