Commit 2024-11-14 00:39 e5869c71

View on Github →

feat(Sym2): Add pmap (#16557) Adds Sym2.pmap and Sym2.attachWith, which is direct application of pmap. These functions are analogous to the functions with the same name under the namespace List and Multiset.

Estimated changes

Modified Mathlib/Data/Sym/Sym2.lean

added def Sym2.attachWith

added theorem Sym2.attachWith_map_subtypeVal

added theorem Sym2.forall_mem_pair

added theorem Sym2.map_pmap

added theorem Sym2.mem_pmap_iff

added theorem Sym2.pair_eq_pmap

added def Sym2.pmap

added theorem Sym2.pmap_eq_map

added theorem Sym2.pmap_map

added theorem Sym2.pmap_pair

added theorem Sym2.pmap_pmap

added theorem Sym2.pmap_subtype_map_subtypeVal