feat(Combinatorics/SimpleGraph/Operations): a graph is the supremum of edge graphs (leanprover-community#39561)

- `G = ⨆ e ∈ G.edgeSet, fromEdgeSet {e}`
- `G = sSup { edge u v | (u : V) (v : V) (_ : G.Adj u v) }`

and `edgeSet` & `fromEdgeSet` preserve sup & inf.

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Basic.lean

@@ -526,6 +526,27 @@ theorem edgeSet_inf : (G₁ ⊓ G₂).edgeSet = G₁.edgeSet ∩ G₂.edgeSet :=
   ext ⟨x, y⟩
   rfl
 
+theorem edgeSet_sSup {s : Set (SimpleGraph V)} : (sSup s).edgeSet = ⋃₀ (edgeSet '' s) := by
+  ext ⟨x, y⟩
+  simp
+
+theorem edgeSet_sInf {s : Set (SimpleGraph V)} (h : s.Nonempty) :
+    (sInf s).edgeSet = ⋂₀ (edgeSet '' s) := by
+  ext ⟨x, y⟩
+  have ⟨G, hG⟩ := h
+  simpa using (· G hG |>.ne)
+
+theorem edgeSet_iSup {ι : Sort*} {f : ι → SimpleGraph V} :
+    (⨆ i, f i).edgeSet = ⋃ i, (f i).edgeSet := by
+  ext ⟨x, y⟩
+  simp
+
+theorem edgeSet_iInf {ι : Sort*} [Nonempty ι] {f : ι → SimpleGraph V} :
+    (⨅ i, f i).edgeSet = ⋂ i, (f i).edgeSet := by
+  ext ⟨x, y⟩
+  have ⟨i⟩ := ‹Nonempty ι›
+  simpa using (· i |>.ne)
+
 @[simp]
 theorem edgeSet_sdiff : (G₁ \ G₂).edgeSet = G₁.edgeSet \ G₂.edgeSet := by
   ext ⟨x, y⟩
@@ -670,6 +691,27 @@ theorem fromEdgeSet_union (s t : Set (Sym2 V)) :
   ext v w
   simp [Set.mem_union, or_and_right]
 
+theorem fromEdgeSet_sUnion {s : Set (Set (Sym2 V))} :
+    fromEdgeSet (⋃₀ s) = sSup (fromEdgeSet '' s) := by
+  ext u v
+  simp
+  grind
+
+theorem fromEdgeSet_iUnion {ι : Sort*} {f : ι → Set (Sym2 V)} :
+    fromEdgeSet (⋃ i, f i) = ⨆ i, fromEdgeSet (f i) := by
+  ext u v
+  simp
+
+theorem fromEdgeSet_sInter {s : Set (Set (Sym2 V))} :
+    fromEdgeSet (⋂₀ s) = sInf (fromEdgeSet '' s) := by
+  ext u v
+  simp_all
+
+theorem fromEdgeSet_iInter {ι : Sort*} {f : ι → Set (Sym2 V)} :
+    fromEdgeSet (⋂ i, f i) = ⨅ i, fromEdgeSet (f i) := by
+  ext u v
+  simp_all
+
 @[simp]
 theorem fromEdgeSet_sdiff (s t : Set (Sym2 V)) :
     fromEdgeSet (s \ t) = fromEdgeSet s \ fromEdgeSet t := by

Mathlib/Combinatorics/SimpleGraph/Operations.lean

@@ -195,6 +195,15 @@ lemma disjoint_edge {u v : V} : Disjoint G (edge u v) ↔ ¬G.Adj u v := by
 lemma sdiff_edge {u v : V} (h : ¬G.Adj u v) : G \ edge u v = G := by
   simp [disjoint_edge, h]
 
+theorem biSup_fromEdgeSet_singleton_eq : ⨆ e ∈ G.edgeSet, fromEdgeSet {e} = G := by
+  simp_rw [← edgeSet_inj, ← iSup_subtype'', edgeSet_iSup, edgeSet_fromEdgeSet, ← Set.iUnion_sdiff,
+    Set.iUnion_coe_set, Set.biUnion_of_singleton]
+  exact Set.disjoint_left.mpr G.edgeSet_subset_compl_diagSet |>.sdiff_eq_left
+
+theorem sSup_edge_eq : sSup { edge u v | (u : V) (v : V) (_ : G.Adj u v) } = G := by
+  refine .trans ?_ G.biSup_fromEdgeSet_singleton_eq
+  simp_rw [edge, ← iSup_subtype'', iSup, Set.range, Subtype.exists, Sym2.exists, mem_edgeSet]
+
 theorem Subgraph.spanningCoe_sup_edge_le {H : Subgraph (G ⊔ edge s t)} (h : ¬ H.Adj s t) :
     H.spanningCoe ≤ G := by
   intro v w hvw