From db098668d1dd2ac83bce0fe3784b4e610d0c0689 Mon Sep 17 00:00:00 2001 From: Hyeokjun Kwon <86776403+Jun2M@users.noreply.github.com> Date: Thu, 31 Oct 2024 12:32:29 -0400 Subject: [PATCH] Update Mathlib/Data/Sym/Sym2.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Yaël Dillies --- Mathlib/Data/Sym/Sym2.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/Sym/Sym2.lean b/Mathlib/Data/Sym/Sym2.lean index 16aabc1450757..78742fa7d8574 100644 --- a/Mathlib/Data/Sym/Sym2.lean +++ b/Mathlib/Data/Sym/Sym2.lean @@ -408,7 +408,7 @@ def pmap {P : α → Prop} (f : ∀ a, P a → β) (s : Sym2 α) : (∀ a ∈ s, /-- "Attach" a proof `P a` that holds for all the elements of `s` to produce a new Sym2 object - with the same elements but in the type `{x // P x}`. +with the same elements but in the type `{x // P x}`. -/ def attachWith (s : Sym2 α) (P : α → Prop) (f : ∀ a ∈ s, P a) : Sym2 {a // P a} := pmap Subtype.mk s f