Commit 2024-09-30 17:40 5024c936

View on Github →

feat: Disjoint G₁.edgeFinset G₂.edgeFinset ↔ Disjoint G₁ G₂ (#17286) From LeanCamCombi

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

added theorem SimpleGraph.disjoint_edgeFinset

added theorem SimpleGraph.edgeFinset_eq_empty

added theorem SimpleGraph.edgeFinset_nonempty