Theorem SimpleGraph.not_mem_edgeSet_of_isDiag

Modification history

2025-11-08 20:46
Mathlib/Combinatorics/SimpleGraph/Basic.lean
feat(SimpleGraph): characterise when the edge set is a given set (#31391) …
Added SimpleGraph.not_mem_edgeSet_of_isDiagView on Github →