From 4ebcc422a776f6c71b4b6b9f9b90b3250aaaa581 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 3 Jul 2024 21:49:08 +0200 Subject: [PATCH] chore: fix docstring --- Mathlib/AlgebraicGeometry/Cover/Open.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/AlgebraicGeometry/Cover/Open.lean b/Mathlib/AlgebraicGeometry/Cover/Open.lean index 3777e1629ce9ff..74c3313f6259b4 100644 --- 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