From d64b678277e81c206bb6382bc3685e4a4cc917ac Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Tue, 6 Feb 2024 07:47:09 +0000 Subject: [PATCH] chore(PartialHomeomorph): `Fintype` -> `Finite` (#10288) --- Mathlib/Topology/PartialHomeomorph.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/PartialHomeomorph.lean b/Mathlib/Topology/PartialHomeomorph.lean index 0b917487584b1..251e94cfd2a35 100644 --- 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. -/