Locally finite families reindexed along a projection

A locally finite family of sets stays locally finite when it is reindexed along the first projection ι × κ → ι with κ finite (LocallyFinite.comp_fst). Together with LocallyFinite.subset, this makes a family indexed by ι × κ whose (i, k)-th member lies in the i-th member of a locally finite family locally finite.

theorem LocallyFinite.comp_fst {ι : Type u_1} {κ : Type u_2} {X : Type u_3} [TopologicalSpace X] {f : ι → Set X} [Finite κ] (hf : LocallyFinite f) : LocallyFinite fun (p : ι × κ) => f p.1

A locally finite family stays locally finite when reindexed along the first projection ι × κ → ι, for κ finite.