theorem Graph.stronglyDisjoint_iff_disjoint_of_compatible {α : Type u_1} {β : Type u_2} {H₁ H₂ : Graph α β} (h : H₁.Compatible H₂) : H₁.StronglyDisjoint H₂ ↔ Disjoint H₁ H₂

theorem Graph.iInter_option_eq_sInter_insert {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G₁ : Graph α β} {G : ι → Graph α β} : (Graph.iInter fun (x : Option ι) => x.elim G₁ G) = Graph.sInter (insert G₁ (Set.range G)) ⋯

theorem Graph.isClosedSubgraph_iUnion_of_stronglyDisjoint {α : Type u_1} {β : Type u_2} {ι : Type u_3} {Hι : ι → Graph α β} (h : Pairwise (Function.onFun StronglyDisjoint Hι)) (i : ι) : (Hι i).IsClosedSubgraph (Graph.iUnion Hι ⋯)

theorem Graph.isClosedSubgraph_sUnion_of_stronglyDisjoint {α : Type u_1} {β : Type u_2} {G : Graph α β} (s : Set (Graph α β)) (hs : s.Pairwise StronglyDisjoint) (hG : G ∈ s) : G.IsClosedSubgraph (Graph.sUnion s ⋯)

theorem Graph.isClosedSubgraph_union_left_of_vertexSet_disjoint {α : Type u_1} {β : Type u_2} {H₁ H₂ : Graph α β} (h : Disjoint H₁.vertexSet H₂.vertexSet) : H₁.IsClosedSubgraph (H₁ ∪ H₂)

theorem Graph.Disjoint.isClosedSubgraph_union_left {α : Type u_1} {β : Type u_2} {H₁ H₂ : Graph α β} (h : Disjoint H₁ H₂) : H₁.IsClosedSubgraph (H₁ ∪ H₂)

theorem Graph.StronglyDisjoint.isClosedSubgraph_union_left {α : Type u_1} {β : Type u_2} {H₁ H₂ : Graph α β} (h : H₁.StronglyDisjoint H₂) : H₁.IsClosedSubgraph (H₁ ∪ H₂)

theorem Graph.StronglyDisjoint.isClosedSubgraph_union_right {α : Type u_1} {β : Type u_2} {H₁ H₂ : Graph α β} (h : H₁.StronglyDisjoint H₂) : H₂.IsClosedSubgraph (H₁ ∪ H₂)

theorem Graph.IsClosedSubgraph.union {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (h₁ : H₁.IsClosedSubgraph G) (h₂ : H₂.IsClosedSubgraph G) : (H₁ ∪ H₂).IsClosedSubgraph G

theorem Graph.IsSpanningSubgraph.union {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (h₁ : H₁ ≤s G) (h₂ : H₂ ≤s G) : H₁ ∪ H₂ ≤s G

theorem Graph.IsSpanningSubgraph.union_left {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (h₁ : H₁ ≤s G) (h₂ : H₂ ≤ G) : H₁ ∪ H₂ ≤s G

theorem Graph.IsSpanningSubgraph.union_right {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (h₁ : H₁ ≤ G) (h₂ : H₂ ≤s G) : H₁ ∪ H₂ ≤s G

theorem Graph.IsInducedSubgraph.inter {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (h₁ : H₁.IsInducedSubgraph G) (h₂ : H₂.IsInducedSubgraph G) : (H₁ ∩ H₂).IsInducedSubgraph G

theorem Graph.IsClosedSubgraph.inter {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (h₁ : H₁.IsClosedSubgraph G) (h₂ : H₂.IsClosedSubgraph G) : (H₁ ∩ H₂).IsClosedSubgraph G

theorem Graph.IsClosedSubgraph.inter_le {α : Type u_1} {β : Type u_2} {K G H : Graph α β} (hKG : K.IsClosedSubgraph G) (hle : H ≤ G) : (K ∩ H).IsClosedSubgraph H

Adding one edge

theorem Graph.addEdge_deleteEdge {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (he : e ∉ G.edgeSet) (hx : x ∈ G.vertexSet) (hy : y ∈ G.vertexSet) : (G.addEdge e x y).deleteEdges {e} = G

theorem Graph.addEdge_mono {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β} (hle : H ≤ G) : H.addEdge e x y ≤ G.addEdge e x y

theorem Graph.deleteEdge_le_addEdge {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} : G.deleteEdges {e} ≤ G.addEdge e x y

theorem Graph.deleteEdge_addEdge {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} : (G.deleteEdges {e}).addEdge e x y = G.addEdge e x y

theorem Graph.isSpanningSubgraph_addEdge {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (he : e ∉ G.edgeSet) (hx : x ∈ G.vertexSet) (hy : y ∈ G.vertexSet) : G ≤s G.addEdge e x y

theorem Graph.IsLink.deleteEdge_addEdge {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) : (G.deleteEdges {e}).addEdge e x y = G