feat(Combinatorics/SimpleGraph/Basic): Disjoint for graph sets (leanprover-community#41795)

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Basic.lean

@@ -13,6 +13,8 @@ public import Mathlib.Data.Sym.Sym2
 public import Mathlib.Order.CompleteBooleanAlgebra
 public import Mathlib.Tactic.CrossRefAttribute
 
+import Mathlib.Data.Set.Lattice
+
 /-!
 # Simple graphs
 
@@ -155,7 +157,7 @@ def completeBipartiteGraph (V W : Type*) : SimpleGraph (V ⊕ W) where
 
 namespace SimpleGraph
 
-variable {ι : Sort*} {V : Type u} (G : SimpleGraph V) {a b c u v w : V} {e : Sym2 V}
+variable {ι : Sort*} {V : Type u} (G H : SimpleGraph V) {a b c u v w : V} {e : Sym2 V}
 
 @[simp]
 protected theorem irrefl {v : V} : ¬G.Adj v v :=
@@ -553,6 +555,11 @@ variable {G G₁ G₂}
 @[simp] lemma disjoint_edgeSet : Disjoint G₁.edgeSet G₂.edgeSet ↔ Disjoint G₁ G₂ := by
   rw [Set.disjoint_iff, disjoint_iff_inf_le, ← edgeSet_inf, ← edgeSet_bot, OrderEmbedding.le_iff_le]
 
+theorem disjoint_of_disjoint_support (h : Disjoint G.support H.support) : Disjoint G H := by
+  simp_rw [Set.disjoint_left, mem_support] at h
+  rw [← disjoint_edgeSet, Set.disjoint_left, Sym2.forall]
+  grind [mem_edgeSet]
+
 @[simp] lemma edgeSet_eq_empty : G.edgeSet = ∅ ↔ G = ⊥ := by rw [← edgeSet_bot, edgeSet_inj]
 
 @[simp] lemma edgeSet_nonempty : G.edgeSet.Nonempty ↔ G ≠ ⊥ := by
@@ -755,6 +762,17 @@ theorem mk'_mem_incidenceSet_right_iff : s(a, b) ∈ G.incidenceSet b ↔ G.Adj
 theorem edge_mem_incidenceSet_iff {e : G.edgeSet} : ↑e ∈ G.incidenceSet a ↔ a ∈ (e : Sym2 V) :=
   and_iff_right e.2
 
+theorem iUnion_incidenceSet : ⋃ v, G.incidenceSet v = G.edgeSet := by
+  ext ⟨_, _⟩
+  simp [mk'_mem_incidenceSet_iff]
+
+variable {G H} in
+theorem disjoint_incidenceSet :
+    (∀ v, Disjoint (G.incidenceSet v) (H.incidenceSet v)) ↔ Disjoint G H := by
+  simp_rw [← disjoint_edgeSet, ← iUnion_incidenceSet, Set.disjoint_iUnion_left,
+    Set.disjoint_iUnion_right, Set.disjoint_left, Sym2.forall]
+  grind [mk'_mem_incidenceSet_iff]
+
 theorem incidenceSet_inter_incidenceSet_subset (h : a ≠ b) :
     G.incidenceSet a ∩ G.incidenceSet b ⊆ {s(a, b)} := fun _e he =>
   (Sym2.mem_and_mem_iff h).1 ⟨he.1.2, he.2.2⟩
@@ -798,6 +816,11 @@ variable (v) in
 theorem neighborSet_ne_univ : G.neighborSet v ≠ .univ :=
   Set.ne_univ_iff_exists_notMem _ |>.mpr ⟨v, G.notMem_neighborSet_self⟩
 
+variable {G H} in
+theorem disjoint_neighborSet :
+    (∀ v, Disjoint (G.neighborSet v) (H.neighborSet v)) ↔ Disjoint G H := by
+  simp_rw [← disjoint_edgeSet, Set.disjoint_left, mem_neighborSet, Sym2.forall, mem_edgeSet]
+
 @[simp]
 theorem mem_incidenceSet (v w : V) : s(v, w) ∈ G.incidenceSet v ↔ G.Adj v w := by
   simp [incidenceSet]
@@ -890,6 +913,12 @@ instance decidableMemCommonNeighbors [DecidableRel G.Adj] (v w : V) :
     DecidablePred (· ∈ G.commonNeighbors v w) :=
   inferInstanceAs <| DecidablePred fun u => u ∈ G.neighborSet v ∧ u ∈ G.neighborSet w
 
+variable {G H} in
+theorem disjoint_commonNeighbors :
+    (∀ u v, Disjoint (G.commonNeighbors u v) (H.commonNeighbors u v)) ↔ Disjoint G H := by
+  simp_rw [← disjoint_edgeSet, Set.disjoint_left, mem_commonNeighbors, Sym2.forall, mem_edgeSet]
+  grind
+
 theorem commonNeighbors_top_eq {v w : V} :
     (⊤ : SimpleGraph V).commonNeighbors v w = Set.univ \ {v, w} := by
   ext u

Mathlib/Combinatorics/SimpleGraph/Finite.lean

@@ -47,7 +47,7 @@ open Finset Function
 
 namespace SimpleGraph
 
-variable {V : Type*} (G : SimpleGraph V) {e : Sym2 V}
+variable {V : Type*} (G H : SimpleGraph V) {e : Sym2 V}
 
 section EdgeFinset
 
@@ -197,6 +197,10 @@ protected alias ⟨IsIsolated.of_neighborFinset_eq_empty, IsIsolated.neighborFin
 
 attribute [simp] IsIsolated.neighborFinset_eq_empty
 
+theorem disjoint_neighborFinset_of_disjoint [Fintype <| H.neighborSet v] (h : Disjoint G H) :
+    Disjoint (G.neighborFinset v) (H.neighborFinset v) := by
+  simp [← Finset.disjoint_coe, disjoint_neighborSet.mpr h v]
+
 /-- `G.degree v` is the number of vertices adjacent to `v`. -/
 def degree : ℕ := #(G.neighborFinset v)
 
@@ -289,6 +293,10 @@ theorem incidenceFinset_subset [DecidableEq V] [Fintype G.edgeSet] :
     G.incidenceFinset v ⊆ G.edgeFinset :=
   Set.toFinset_subset_toFinset.mpr (G.incidenceSet_subset v)
 
+theorem disjoint_incidenceFinset_of_disjoint [DecidableEq V] [Fintype <| H.neighborSet v]
+    (h : Disjoint G H) : Disjoint (G.incidenceFinset v) (H.incidenceFinset v) := by
+  simp [← Finset.disjoint_coe, disjoint_incidenceSet.mpr h v]
+
 /-- The degree of a vertex is at most the number of edges. -/
 theorem degree_le_card_edgeFinset [Fintype G.edgeSet] :
     G.degree v ≤ #G.edgeFinset := by