Skip to content

Commit

Permalink
Update Mathlib/Data/Sym/Sym2.lean
Browse files Browse the repository at this point in the history
Co-authored-by: Yaël Dillies <[email protected]>
  • Loading branch information
Jun2M and YaelDillies authored Oct 31, 2024
1 parent 5cb9f54 commit db09866
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Data/Sym/Sym2.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit db09866

Please sign in to comment.