Commit 2023-12-27 05:26 9ed6b90f

View on Github →

refactor: remove Sym2's global Prod setoid instance, use s(x, y) notation for unordered pairs (#8729) The Sym2 type used a global setoid instance on α × α so that ⟦(x, y)⟧ could stand for an unordered pair using standard Quotient syntax. This commit refactors Sym2 to not use Quotient and instead use its own s(x, y) notation. One benefit to this is that this notation produces a term with type Sym2 rather than Quotient. The Fintype instance for Sym2 is in Mathlib.Data.Finset.Sym. We switch from using the one for Quotient because it does not require DecidableEq.

Estimated changes

modified theorem SimpleGraph.Dart.edge_mk
modified theorem SimpleGraph.fromEdgeSet_adj
modified theorem SimpleGraph.mem_edgeSet
modified theorem Finset.mk_mem_sym2_iff
modified theorem Finset.sym2_eq_image
modified theorem Sym2.card_image_diag
added def Sym2.Rel.setoid
modified theorem Sym2.ball
modified theorem Sym2.congr_left
modified theorem Sym2.congr_right
modified def Sym2.diag
modified theorem Sym2.eq_iff
modified theorem Sym2.eq_swap
modified theorem Sym2.fromRel_proj_prop
modified theorem Sym2.fromRel_prop
modified theorem Sym2.isDiag_iff_proj_eq
deleted theorem Sym2.lift_mk''
added theorem Sym2.lift_mk
deleted theorem Sym2.lift₂_mk''
added theorem Sym2.lift₂_mk
modified theorem Sym2.map_pair_eq
modified theorem Sym2.mem_and_mem_iff
modified theorem Sym2.mem_iff'
modified theorem Sym2.mem_iff
modified theorem Sym2.mem_iff_exists
deleted theorem Sym2.mem_mk''_left
deleted theorem Sym2.mem_mk''_right
added theorem Sym2.mem_mk_left
added theorem Sym2.mem_mk_right
deleted theorem Sym2.mk''_eq_mk''_iff
deleted theorem Sym2.mk''_isDiag_iff
deleted theorem Sym2.mk''_prod_swap_eq
added theorem Sym2.mk_eq_mk_iff
added theorem Sym2.mk_isDiag_iff
added theorem Sym2.mk_prod_swap_eq
modified theorem Sym2.other_spec'
modified theorem Sym2.other_spec
added theorem Sym2.rel_iff'
modified theorem Sym2.rel_iff
modified theorem Sym2.toRel_prop
modified def Sym2
modified theorem Sym2.GameAdd.fst
modified theorem Sym2.GameAdd.fst_snd
modified theorem Sym2.GameAdd.snd
modified theorem Sym2.GameAdd.snd_fst
modified theorem Sym2.gameAdd_iff