chore: fix docstring (#14392)

An unused finiteness assumption is removed from the docstring of a lemma.
leanprover-community · Jul 3, 2024 · e6737c3 · e6737c3
1 parent ce981a6
commit e6737c3
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/AlgebraicGeometry/Cover/Open.lean b/Mathlib/AlgebraicGeometry/Cover/Open.lean
@@ -397,7 +397,7 @@ def OpenCover.fromAffineRefinement {X : Scheme.{u}} (𝓤 : X.OpenCover) :
   idx j := j.fst
   app j := (𝓤.obj j.fst).affineCover.map _
 
-/-- If two global sections agree after restriction to each member of a finite open cover, then
+/-- If two global sections agree after restriction to each member of an open cover, then
 they agree globally. -/
 lemma OpenCover.ext_elem {X : Scheme.{u}} {U : Opens X} (f g : Γ(X, U)) (𝒰 : X.OpenCover)
     (h : ∀ i : 𝒰.J, (𝒰.map i).app U f = (𝒰.map i).app U g) : f = g := by