chore(topology/basic): use finite in locally_finite_of_finite (#15181)

Rename `locally_finite_of_fintype` to `locally_finite_of_finite`, use `[finite]` instead of `[fintype]`.

Author: urkud

src/topology/basic.lean

@@ -1191,7 +1191,7 @@ lemma locally_finite.point_finite {f : β → set α} (hf : locally_finite f) (x
   {b | x ∈ f b}.finite :=
 let ⟨t, hxt, ht⟩ := hf x in ht.subset $ λ b hb, ⟨x, hb, mem_of_mem_nhds hxt⟩
 
-lemma locally_finite_of_fintype [fintype β] (f : β → set α) : locally_finite f :=
+lemma locally_finite_of_finite [finite β] (f : β → set α) : locally_finite f :=
 assume x, ⟨univ, univ_mem, to_finite _⟩
 
 lemma locally_finite.subset

src/topology/paracompact.lean

@@ -112,7 +112,7 @@ begin
   rcases compact_univ.elim_finite_subcover _ ho hu.ge with ⟨T, hT⟩,
   have := hT, simp only [subset_def, mem_Union] at this,
   choose i hiT hi using λ x, this x (mem_univ x),
-  refine ⟨(T : set ι), λ t, s t, λ t, ho _, _, locally_finite_of_fintype _, λ t, ⟨t, subset.rfl⟩⟩,
+  refine ⟨(T : set ι), λ t, s t, λ t, ho _, _, locally_finite_of_finite _, λ t, ⟨t, subset.rfl⟩⟩,
   simpa only [Union_coe_set, ← univ_subset_iff]
 end