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

From LeanCamCombi
leanprover-community · Sep 30, 2024 · 5024c93 · 5024c93
1 parent 445d05d
commit 5024c93
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/Mathlib/Combinatorics/SimpleGraph/Finite.lean b/Mathlib/Combinatorics/SimpleGraph/Finite.lean
@@ -92,6 +92,15 @@ theorem edgeFinset_inf [DecidableEq V] : (G₁ ⊓ G₂).edgeFinset = G₁.edgeF
 theorem edgeFinset_sdiff [DecidableEq V] :
     (G₁ \ G₂).edgeFinset = G₁.edgeFinset \ G₂.edgeFinset := by simp [edgeFinset]
 
+lemma disjoint_edgeFinset : Disjoint G₁.edgeFinset G₂.edgeFinset ↔ Disjoint G₁ G₂ := by
+  simp_rw [← Finset.disjoint_coe, coe_edgeFinset, disjoint_edgeSet]
+
+lemma edgeFinset_eq_empty : G.edgeFinset = ∅ ↔ G = ⊥ := by
+  rw [← edgeFinset_bot, edgeFinset_inj]
+
+lemma edgeFinset_nonempty : G.edgeFinset.Nonempty ↔ G ≠ ⊥ := by
+  rw [Finset.nonempty_iff_ne_empty, edgeFinset_eq_empty.ne]
+
 theorem edgeFinset_card : G.edgeFinset.card = Fintype.card G.edgeSet :=
   Set.toFinset_card _