Theorem SimpleGraph.edgeSet_eq_iff

Modification history

2025-12-01 17:55

Mathlib/Combinatorics/SimpleGraph/Basic.lean

feat(Combinatorics/SimpleGraph): use `Sym2.diagSet` instead of explicit sets (#32255)

Modified SimpleGraph.edgeSet_eq_iff View on Github →

2025-11-08 20:46

Mathlib/Combinatorics/SimpleGraph/Basic.lean

feat(SimpleGraph): characterise when the edge set is a given set (#31391) …

Added SimpleGraph.edgeSet_eq_iff View on Github →