Commit 2026-01-24 20:18 be04ab25

View on Github →

chore(Data/Sym2): improve defeq of diagSet (#32679) #30559 introduced a regression on the defeqs in the SimpleGraph API. This PR fixes it. From LeanCamCombi

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

added theorem SimpleGraph.edgeSet_subset_compl_diagSet

deleted theorem SimpleGraph.edgeSet_subset_setOf_not_isDiag

Modified Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean

Modified Mathlib/Combinatorics/SimpleGraph/Operations.lean

modified theorem SimpleGraph.edge_edgeSet_of_ne

Modified Mathlib/Data/Sym/Card.lean

modified theorem Sym2.card_diagSet_compl

Modified Mathlib/Data/Sym/Sym2.lean

modified def Sym2.diagSet

modified theorem Sym2.diagSet_eq_setOf_isDiag

modified theorem Sym2.diagSet_eq_univ_of_subsingleton

added theorem Sym2.diagSet_subset_fromRel

added theorem Sym2.disjoint_diagSet_fromRel

added theorem Sym2.fromRel_subset_compl_diagSet

modified theorem Sym2.isDiag_iff_mem_range_diag

modified theorem Sym2.isDiag_map

modified theorem Sym2.isDiag_of_subsingleton

added theorem Sym2.mem_diagSet

modified theorem Sym2.mem_diagSet_iff_eq

modified theorem Sym2.mem_diagSet_iff_isDiag

added theorem Sym2.range_diag