chore(PartialHomeomorph): Fintype -> Finite (#10288)

leanprover-community · Feb 6, 2024 · d64b678 · d64b678
1 parent a76d5c1
commit d64b678
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Topology/PartialHomeomorph.lean b/Mathlib/Topology/PartialHomeomorph.lean
@@ -1092,7 +1092,7 @@ end Prod
 /- finite product of partial homeomorphisms -/
 section Pi
 
-variable {ι : Type*} [Fintype ι] {X Y : ι → Type*} [∀ i, TopologicalSpace (X i)]
+variable {ι : Type*} [Finite ι] {X Y : ι → Type*} [∀ i, TopologicalSpace (X i)]
   [∀ i, TopologicalSpace (Y i)] (ei : ∀ i, PartialHomeomorph (X i) (Y i))
 
 /-- The product of a finite family of `PartialHomeomorph`s. -/