feat(Data/Set/Finite): union of infinitely many sets is infinite (#15447

)

We add three separate versions of the statement that the union of an infinite collection of sets is infinite.

Mathlib/Data/Set/Finite.lean

@@ -1271,6 +1271,22 @@ theorem not_injOn_infinite_finite_image {f : α → β} {s : Set α} (h_inf : s.
   contrapose! h
   rwa [injective_codRestrict, ← injOn_iff_injective]
 
+theorem infinite_iUnion {ι : Type*} [Infinite ι] {s : ι → Set α} (hs : Function.Injective s) :
+    (⋃ i, s i).Infinite :=
+  fun hfin ↦ @not_injective_infinite_finite ι _ _ hfin.finite_subsets.to_subtype
+    (fun i ↦ ⟨s i, subset_iUnion _ _⟩) fun i j h_eq ↦ hs (by simpa using h_eq)
+
+theorem Infinite.biUnion {ι : Type*} {s : ι → Set α} {a : Set ι} (ha : a.Infinite)
+    (hs : a.InjOn s) : (⋃ i ∈ a, s i).Infinite := by
+  rw [biUnion_eq_iUnion]
+  have _ := ha.to_subtype
+  exact infinite_iUnion fun ⟨i,hi⟩ ⟨j,hj⟩ hij ↦ by simp [hs hi hj hij]
+
+theorem Infinite.sUnion {s : Set (Set α)} (hs : s.Infinite) : (⋃₀ s).Infinite := by
+  rw [sUnion_eq_iUnion]
+  have _ := hs.to_subtype
+  exact infinite_iUnion Subtype.coe_injective
+
 /-! ### Order properties -/
 
 section Preorder