Theorem SimpleGraph.edgeFinset_nonempty

Modification history

2024-09-30 17:40
Mathlib/Combinatorics/SimpleGraph/Finite.lean
feat: `Disjoint G₁.edgeFinset G₂.edgeFinset ↔ Disjoint G₁ G₂` (#17286) …
Added SimpleGraph.edgeFinset_nonemptyView on Github →