@[simp]

theorem Graph.restrict_isNonloopAt_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {F : Set β} : (G.restrict F).IsNonloopAt e x ↔ G.IsNonloopAt e x ∧ e ∈ F

theorem Graph.neighbor_restrict_subset {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) (x : α) : N(G.restrict F, x) ⊆ N(G, x)

theorem Graph.setNeighbor_restrict_subset {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) (S : Set α) : N(G.restrict F, S) ⊆ N(G, S)

@[simp]

theorem Graph.incEdges_restrict {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) (x : α) : E(G.restrict F, x) = E(G, x) ∩ F

@[simp]

theorem Graph.setIncEdges_restrict {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) (S : Set α) : E(G.restrict F, S) = E(G, S) ∩ F

theorem Graph.endSet_restrict {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) [DecidablePred fun (x : β) => x ∈ F] (e : β) : V(G.restrict F, e) = if e ∈ F then V(G, e) else ∅

@[simp]

theorem Graph.endSet_restrict_of_mem {α : Type u_1} {β : Type u_2} {e : β} (G : Graph α β) (F : Set β) (he : e ∈ F) : V(G.restrict F, e) = V(G, e)

@[simp]

theorem Graph.endSet_restrict_of_not_mem {α : Type u_1} {β : Type u_2} {e : β} (G : Graph α β) (F : Set β) (he : e ∉ F) : V(G.restrict F, e) = ∅

@[simp]

theorem Graph.linkEdges_restrict {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) (u v : α) : E(G.restrict F, u, v) = E(G, u, v) ∩ F

@[simp]

theorem Graph.setLinkEdges_restrict {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) (S T : Set α) : E(G.restrict F, S, T) = E(G, S, T) ∩ F

theorem Graph.restrict_le_restrict {α : Type u_1} {β : Type u_2} {G : Graph α β} {F₁ F₂ : Set β} (h : G.edgeSet ∩ F₁ ⊆ G.edgeSet ∩ F₂) : G.restrict F₁ ≤ G.restrict F₂

theorem Graph.restrict_le_restrict_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (F₁ F₂ : Set β) : G.restrict F₁ ≤ G.restrict F₂ ↔ G.edgeSet ∩ F₁ ⊆ G.edgeSet ∩ F₂

theorem Graph.restrict_of_superset {α : Type u_1} {β : Type u_2} {F : Set β} (G : Graph α β) (hF : G.edgeSet ⊆ F) : G.restrict F = G

theorem Graph.restrict_eq_restrict {α : Type u_1} {β : Type u_2} {G : Graph α β} {F₁ F₂ : Set β} (h : G.edgeSet ∩ F₁ = G.edgeSet ∩ F₂) : G.restrict F₁ = G.restrict F₂

theorem Graph.restrict_eq_restrict_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (F₁ F₂ : Set β) : G.restrict F₁ = G.restrict F₂ ↔ G.edgeSet ∩ F₁ = G.edgeSet ∩ F₂

@[simp]

theorem Graph.le_restrict_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} {F : Set β} : H ≤ G.restrict F ↔ H ≤ G ∧ H.edgeSet ⊆ F

@[simp]

theorem Graph.restrict_isSpanningSubgraph {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} : G.restrict F ≤s G

theorem Graph.restrict_isSpanningSubgraph_restrict {α : Type u_1} {β : Type u_2} {G : Graph α β} {F₁ F₂ : Set β} (h : G.edgeSet ∩ F₁ ⊆ G.edgeSet ∩ F₂) : G.restrict F₁ ≤s G.restrict F₂

theorem Graph.restrict_isSpanningSubgraph_restrict' {α : Type u_1} {β : Type u_2} {G : Graph α β} {F₁ F₂ : Set β} (h : F₁ ⊆ F₂) : G.restrict F₁ ≤s G.restrict F₂

theorem Graph.restrict_isSpanningSubgraph_restrict_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (F₁ F₂ : Set β) : G.restrict F₁ ≤s G.restrict F₂ ↔ G.edgeSet ∩ F₁ ⊆ G.edgeSet ∩ F₂

theorem Graph.IsSpanningSubgraph.restrict {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H ≤s G) (F : Set β) : H.restrict F ≤s G.restrict F

@[simp]

theorem Graph.deleteEdges_isNonloopAt_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {F : Set β} : (G.deleteEdges F).IsNonloopAt e x ↔ G.IsNonloopAt e x ∧ e ∉ F

theorem Graph.neighbor_deleteEdges_subset {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) (x : α) : N(G.deleteEdges F, x) ⊆ N(G, x)

theorem Graph.setNeighbor_deleteEdges_subset {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) (S : Set α) : N(G.deleteEdges F, S) ⊆ N(G, S)

@[simp]

theorem Graph.incEdges_deleteEdges {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) (x : α) : E(G.deleteEdges F, x) = E(G, x) \ F

@[simp]

theorem Graph.setIncEdges_deleteEdges {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) (S : Set α) : E(G.deleteEdges F, S) = E(G, S) \ F

@[simp]

theorem Graph.endSet_deleteEdges_of_mem {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) (e : β) (he : e ∈ F) : V(G.deleteEdges F, e) = ∅

@[simp]

theorem Graph.endSet_deleteEdges_of_not_mem {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) (e : β) (he : e ∉ F) : V(G.deleteEdges F, e) = V(G, e)

@[simp]

theorem Graph.linkEdges_deleteEdges {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) (u v : α) : E(G.deleteEdges F, u, v) = E(G, u, v) \ F

@[simp]

theorem Graph.deleteEdges_inter_edgeSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} : G.deleteEdges (F ∩ G.edgeSet) = G.deleteEdges F

@[simp]

theorem Graph.edgeSet_deleteEdges_inter {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} : G.deleteEdges (G.edgeSet ∩ F) = G.deleteEdges F

theorem Graph.deleteEdges_anti_right {α : Type u_1} {β : Type u_2} (G : Graph α β) {F₀ F : Set β} (hss : F₀ ⊆ F) : G.deleteEdges F ≤ G.deleteEdges F₀

theorem Graph.deleteEdges_le_deleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {F₁ F₂ : Set β} (h : G.edgeSet \ F₁ ⊆ G.edgeSet \ F₂) : G.deleteEdges F₁ ≤ G.deleteEdges F₂

theorem Graph.deleteEdges_le_deleteEdges_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (F₁ F₂ : Set β) : G.deleteEdges F₁ ≤ G.deleteEdges F₂ ↔ G.edgeSet \ F₁ ⊆ G.edgeSet \ F₂

@[simp]

theorem Graph.restrict_deleteEdges {α : Type u_1} {β : Type u_2} (G : Graph α β) (F₁ F₂ : Set β) : (G.restrict F₁).deleteEdges F₂ = G.restrict (F₁ \ F₂)

theorem Graph.restrict_deleteEdges_comm {α : Type u_1} {β : Type u_2} (G : Graph α β) (F₁ F₂ : Set β) : (G.restrict F₁).deleteEdges F₂ = (G.deleteEdges F₂).restrict F₁

@[simp]

theorem Graph.deleteEdges_restrict {α : Type u_1} {β : Type u_2} (G : Graph α β) (F₁ F₂ : Set β) : (G.deleteEdges F₁).restrict F₂ = G.restrict (F₂ \ F₁)

theorem Graph.deleteEdges_deleteEdges_comm {α : Type u_1} {β : Type u_2} (G : Graph α β) (F₁ F₂ : Set β) : (G.deleteEdges F₁).deleteEdges F₂ = (G.deleteEdges F₂).deleteEdges F₁

theorem Graph.deleteEdges_eq {α : Type u_1} {β : Type u_2} {F : Set β} (G : Graph α β) (hF : Disjoint G.edgeSet F) : G.deleteEdges F = G

theorem Graph.deleteEdges_eq_of_disjoint {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (hF : Disjoint G.edgeSet F) : G.deleteEdges F = G

theorem Graph.deleteEdges_eq_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) : G.deleteEdges F = G ↔ Disjoint G.edgeSet F

theorem Graph.deleteEdges_eq_deleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {F₁ F₂ : Set β} (h : G.edgeSet \ F₁ = G.edgeSet \ F₂) : G.deleteEdges F₁ = G.deleteEdges F₂

theorem Graph.deleteEdges_eq_deleteEdges_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (F₁ F₂ : Set β) : G.deleteEdges F₁ = G.deleteEdges F₂ ↔ G.edgeSet \ F₁ = G.edgeSet \ F₂

@[simp]

theorem Graph.le_deleteEdges_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} {F : Set β} : H ≤ G.deleteEdges F ↔ H ≤ G ∧ Disjoint H.edgeSet F

theorem Graph.IsNonloopAt.isLoopAt_delete {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsNonloopAt e x) : (G.deleteEdges {e}).IsLoopAt = G.IsLoopAt

theorem Graph.IsLoopAt.isNonloopAt_delete {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsLoopAt e x) : (G.deleteEdges {e}).IsNonloopAt = G.IsNonloopAt

@[simp]

theorem Graph.setLinkEdges_deleteEdges {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) (S T : Set α) : E(G.deleteEdges F, S, T) = E(G, S, T) \ F

@[simp]

theorem Graph.deleteEdges_isSpanningSubgraph {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} : G.deleteEdges F ≤s G

theorem Graph.deleteEdges_isSpanningSubgraph_deleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {F₁ F₂ : Set β} (h : G.edgeSet \ F₁ ⊆ G.edgeSet \ F₂) : G.deleteEdges F₁ ≤s G.deleteEdges F₂

theorem Graph.deleteEdges_isSpanningSubgraph_anti_right {α : Type u_1} {β : Type u_2} {G : Graph α β} {F₁ F₂ : Set β} (h : F₁ ⊆ F₂) : G.deleteEdges F₂ ≤s G.deleteEdges F₁

@[simp]

theorem Graph.deleteEdges_isSpanningSubgraph_deleteEdges_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (F₁ F₂ : Set β) : G.deleteEdges F₁ ≤s G.deleteEdges F₂ ↔ G.edgeSet \ F₁ ⊆ G.edgeSet \ F₂

theorem Graph.IsSpanningSubgraph.deleteEdges {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H ≤s G) (F : Set β) : H.deleteEdges F ≤s G.deleteEdges F

theorem Graph.deleteEdges_eq_noEdge {α : Type u_1} {β : Type u_2} {F : Set β} (G : Graph α β) (hF : G.edgeSet ⊆ F) : G.deleteEdges F = noEdge G.vertexSet β

@[simp]

theorem Graph.noEdge_induce {α : Type u_1} (X Y : Set α) (β : Type u_3) : (noEdge X β)[Y] = noEdge Y β

@[simp]

theorem Graph.noEdge_deleteVerts {α : Type u_1} (X Y : Set α) (β : Type u_3) : (noEdge X β).deleteVerts Y = noEdge (X \ Y) β

@[simp]

theorem Graph.noEdge_delete {α : Type u_1} {β : Type u_2} (X : Set α) (F : Set β) : (noEdge X β).deleteEdges F = noEdge X β

theorem Graph.IsLink.induce {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {X : Set α} (h : G.IsLink e x y) (hx : x ∈ X) (hy : y ∈ X) : G[X].IsLink e x y

@[simp]

theorem Graph.induce_adj_iff {α : Type u_1} {β : Type u_2} {x y : α} {G : Graph α β} {X : Set α} : G[X].Adj x y ↔ G.Adj x y ∧ x ∈ X ∧ y ∈ X

theorem Graph.neighbor_induce {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) [DecidablePred fun (x : α) => x ∈ X] (x : α) : N(G[X], x) = if x ∈ X then N(G, x) ∩ X else ∅

@[simp]

theorem Graph.neighbor_induce_of_notMem {α : Type u_1} {β : Type u_2} {x : α} {X : Set α} (G : Graph α β) (hx : x ∉ X) : N(G[X], x) = ∅

@[simp]

theorem Graph.neighbor_induce_of_mem {α : Type u_1} {β : Type u_2} {x : α} {X : Set α} (G : Graph α β) (hx : x ∈ X) : N(G[X], x) = N(G, x) ∩ X

@[simp]

theorem Graph.setLinkEdges_induce {α : Type u_1} {β : Type u_2} (G : Graph α β) (X S T : Set α) : E(G[X], S, T) = E(G, S ∩ X, T ∩ X)

theorem Graph.linkEdges_induce {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) [DecidablePred fun (x : α) => x ∈ X] (u v : α) : E(G[X], u, v) = if u ∈ X ∧ v ∈ X then E(G, u, v) else ∅

@[simp]

theorem Graph.linkEdges_induce_of_mem {α : Type u_1} {β : Type u_2} {u v : α} {X : Set α} (G : Graph α β) (hu : u ∈ X) (hv : v ∈ X) : E(G[X], u, v) = E(G, u, v)

@[simp]

theorem Graph.linkEdges_induce_of_left_not_mem {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) (u v : α) (hu : u ∉ X) : E(G[X], u, v) = ∅

@[simp]

theorem Graph.linkEdges_induce_of_right_not_mem {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) (u v : α) (hv : v ∉ X) : E(G[X], u, v) = ∅

theorem Graph.Adj.induce {α : Type u_1} {β : Type u_2} {x y : α} {G : Graph α β} {X : Set α} (h : G.Adj x y) (hx : x ∈ X) (hy : y ∈ X) : G[X].Adj x y

@[simp]

theorem Graph.edgeSet_induce_subset {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) : G[X].edgeSet ⊆ G.edgeSet

@[simp]

theorem Graph.induce_inc {α : Type u_1} {β : Type u_2} {x : α} {e : β} (G : Graph α β) (X : Set α) : G[X].Inc e x ↔ G.Inc e x ∧ e ∈ G[X].edgeSet

@[simp]

theorem Graph.induce_singleton_edgeSet {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) : G[{x}].edgeSet = {e : β | G.IsLoopAt e x}

@[simp]

theorem Graph.induce_pair_edgeSet {α : Type u_1} {β : Type u_2} (G : Graph α β) (x y : α) : E(G, x, y) ⊆ G[{x, y}].edgeSet

theorem Graph.IsLink.mem_induce_iff {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {X : Set α} (hG : G.IsLink e x y) : e ∈ G[X].edgeSet ↔ x ∈ X ∧ y ∈ X

theorem Graph.induce_isLink_iff_of_mem_edgeSet {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {X : Set α} (h : e ∈ G[X].edgeSet) : G[X].IsLink e x y ↔ G.IsLink e x y

theorem Graph.induce_induce {α : Type u_1} {β : Type u_2} (G : Graph α β) (X Y : Set α) : G[X][Y] = G[Y].restrict G[X].edgeSet

theorem Graph.compatible_induce {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) : G.Compatible G[X]

theorem Graph.induce_mono_right {α : Type u_1} {β : Type u_2} {X Y : Set α} (G : Graph α β) (hXY : X ⊆ Y) : G[X] ≤ G[Y]

@[simp]

theorem Graph.induce_mono_right_iff {α : Type u_1} {β : Type u_2} {X Y : Set α} (G : Graph α β) : G[X] ≤ G[Y] ↔ X ⊆ Y

theorem Graph.induce_mono_left {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H ≤ G) (X : Set α) : H[X] ≤ G[X]

theorem Graph.induce_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} {X Y : Set α} (h : H ≤ G) (hXY : X ⊆ Y) : H[X] ≤ G[Y]

@[simp]

theorem Graph.induce_eq_self_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) : G[X] = G ↔ X = G.vertexSet

theorem Graph.le_induce_of_le_of_subset {α : Type u_1} {β : Type u_2} {G H : Graph α β} {X : Set α} (h : H ≤ G) (hV : H.vertexSet ⊆ X) : H ≤ G[X]

theorem Graph.le_induce_self {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H ≤ G) : H ≤ G[H.vertexSet]

theorem Graph.le_induce_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} {X : Set α} (hX : X ⊆ G.vertexSet) : H ≤ G[X] ↔ H ≤ G ∧ H.vertexSet ⊆ X

theorem Graph.diff_subset_isolatedSet_induce {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) : X \ G.vertexSet ⊆ G[X].IsolatedSet

@[simp]

theorem Graph.restrict_induce {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) (F : Set β) : (G.restrict F)[X] = G[X].restrict F

@[simp]

theorem Graph.IsSubgraph.induce_restrict_eq {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H ≤ G) : G[H.vertexSet].restrict H.edgeSet = H

@[simp]

theorem Graph.IsSubgraph.restrict_induce_eq {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H ≤ G) : (G.restrict H.edgeSet)[H.vertexSet] = H

theorem Graph.IsSubgraph.vertexSet_diff_subset_isolatedSet_restrict {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H ≤ G) : G.vertexSet \ H.vertexSet ⊆ (G.restrict H.edgeSet).IsolatedSet

theorem Graph.induce_isInducedSubgraph {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α} (hX : X ⊆ G.vertexSet) : G[X].IsInducedSubgraph G

theorem Graph.IsInducedSubgraph.vertexSet_induce_eq {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsInducedSubgraph G) : G[H.vertexSet] = H

theorem Graph.induce_isInducedSubgraph_mono_right {α : Type u_1} {β : Type u_2} {G : Graph α β} {X Y : Set α} (h : X ⊆ Y) : G[X].IsInducedSubgraph G[Y]

@[simp]

theorem Graph.induce_isInducedSubgraph_induce_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (X Y : Set α) : G[X].IsInducedSubgraph G[Y] ↔ X ⊆ Y

theorem Graph.isSpanningSubgraph_of_induce {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H ≤ G) (X : Set α) : H[X] ≤s G[X]

theorem Graph.IsInducedSubgraph.exists_eq_induce {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsInducedSubgraph G) : ∃ X ⊆ G.vertexSet, H = G[X]

An induced subgraph is precisely a subgraph of the form G[X] for some X ⊆ V(G). This version of the lemma can be used with subst or obtain rfl to replace H with G[X].

theorem Graph.IsInducedSubgraph.eq_of_isSpanningSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hi : H.IsInducedSubgraph G) (hs : H ≤s G) : H = G

@[simp]

theorem Graph.induce_isInducedSubgraph_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {X : Set α} : G[X].IsInducedSubgraph G ↔ X ⊆ G.vertexSet

@[simp]

theorem Graph.deleteVerts_isInducedSubgraph {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) : (G.deleteVerts X).IsInducedSubgraph G

@[simp]

theorem Graph.deleteVerts_eq_bot_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) : G.deleteVerts X = ⊥ ↔ G.vertexSet ⊆ X

@[simp]

theorem Graph.bot_deleteVerts {α : Type u_1} {β : Type u_2} {X : Set α} : ⊥.deleteVerts X = ⊥

@[simp]

theorem Graph.deleteVerts_adj_iff {α : Type u_1} {β : Type u_2} {x y : α} (G : Graph α β) (X : Set α) : (G.deleteVerts X).Adj x y ↔ G.Adj x y ∧ x ∉ X ∧ y ∉ X

theorem Graph.neighbor_deleteVerts {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) [DecidablePred fun (x : α) => x ∈ X] (x : α) : N(G.deleteVerts X, x) = if x ∉ X then N(G, x) \ X else ∅

@[simp]

theorem Graph.neighbor_deleteVerts_of_mem {α : Type u_1} {β : Type u_2} {x : α} {X : Set α} (G : Graph α β) (hx : x ∈ X) : N(G.deleteVerts X, x) = ∅

@[simp]

theorem Graph.neighbor_deleteVerts_of_notMem {α : Type u_1} {β : Type u_2} {x : α} {X : Set α} (G : Graph α β) (hx : x ∉ X) : N(G.deleteVerts X, x) = N(G, x) \ X

@[simp]

theorem Graph.deleteVerts_vertexSet_inter {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) : G.deleteVerts (G.vertexSet ∩ X) = G.deleteVerts X

@[simp]

theorem Graph.deleteVerts_eq_self_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) : G.deleteVerts X = G ↔ Disjoint G.vertexSet X

theorem Graph.IsLink.mem_deleteVerts_iff {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {X : Set α} (hG : G.IsLink e x y) : e ∈ (G.deleteVerts X).edgeSet ↔ x ∉ X ∧ y ∉ X

theorem Graph.IsLink.not_mem_incidentEdges {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {X : Set α} (h : (G.deleteVerts X).IsLink e x y) : e ∉ E(G, X)

@[simp]

theorem Graph.Inc.not_mem_of_mem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {X : Set α} (h : G.Inc e x) (hx : x ∈ X) : e ∉ (G.deleteVerts X).edgeSet

theorem Graph.Inc.not_mem_incEdges {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {X : Set α} (h : (G.deleteVerts X).Inc e x) : e ∉ E(G, X)

theorem Graph.Inc.not_mem_of_deleteVerts {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {X : Set α} (h : (G.deleteVerts X).Inc e x) : x ∉ X

@[simp]

theorem Graph.deleteVerts_inc_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} (G : Graph α β) (X : Set α) : (G.deleteVerts X).Inc e x ↔ G.Inc e x ∧ e ∉ E(G, X)

@[simp]

theorem Graph.incEdges_deleteVerts {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) (x : α) : E(G.deleteVerts X, x) = E(G, x) \ E(G, X)

@[simp]

theorem Graph.setIncEdges_deleteVerts {α : Type u_1} {β : Type u_2} (G : Graph α β) (X S : Set α) : E(G.deleteVerts X, S) = E(G, S) \ E(G, X)

@[simp]

theorem Graph.linkEdges_deleteVerts {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) (u v : α) : E(G.deleteVerts X, u, v) = E(G, u, v) \ E(G, X)

theorem Graph.deleteVerts_mono_left {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H ≤ G) (X : Set α) : H.deleteVerts X ≤ G.deleteVerts X

theorem Graph.deleteVerts_anti_right {α : Type u_1} {β : Type u_2} {X Y : Set α} (G : Graph α β) (hXY : X ⊆ Y) : G.deleteVerts Y ≤ G.deleteVerts X

theorem Graph.restrict_deleteVerts {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) (D : Set α) : (G.restrict F).deleteVerts D = (G.deleteVerts D).restrict F

@[simp]

theorem Graph.deleteEdges_induce {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) (F : Set β) : (G.deleteEdges F)[X] = G[X].deleteEdges F

@[simp]

theorem Graph.induce_deleteVerts {α : Type u_1} {β : Type u_2} (G : Graph α β) (X D : Set α) : G[X].deleteVerts D = G[X \ D]

@[simp]

theorem Graph.deleteEdges_deleteVerts {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β) (X : Set α) : (G.deleteEdges F).deleteVerts X = (G.deleteVerts X).deleteEdges F

theorem Graph.deleteVerts_deleteEdges_incidentEdges {α : Type u_1} {β : Type u_2} (G : Graph α β) (X : Set α) : (G.deleteEdges E(G, X)).deleteVerts X = G.deleteVerts X

theorem Graph.deleteVerts_deleteVerts {α : Type u_1} {β : Type u_2} (G : Graph α β) (X Y : Set α) : (G.deleteVerts X).deleteVerts Y = G.deleteVerts (X ∪ Y)

theorem Graph.deleteVerts_deleteVerts_comm {α : Type u_1} {β : Type u_2} (G : Graph α β) (X Y : Set α) : (G.deleteVerts X).deleteVerts Y = (G.deleteVerts Y).deleteVerts X

@[simp]

theorem Graph.le_deleteVerts_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} {X : Set α} : H ≤ G.deleteVerts X ↔ H ≤ G ∧ Disjoint H.vertexSet X

theorem Graph.deleteVerts_le_deleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {X : Set α} (h : ∀ e ∈ G.edgeSet ∩ F, ∃ x ∈ X, G.Inc e x) : G.deleteVerts X ≤ G.deleteEdges F

@[simp]

theorem Graph.deleteVerts_isInducedSubgraph_deleteVerts_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (X Y : Set α) : (G.deleteVerts X).IsInducedSubgraph (G.deleteVerts Y) ↔ G.vertexSet \ X ⊆ G.vertexSet \ Y

theorem Graph.IsInducedSubgraph.deleteVerts {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsInducedSubgraph G) (X : Set α) : (H.deleteVerts X).IsInducedSubgraph (G.deleteVerts X)

theorem Graph.IsSpanningSubgraph.deleteVerts {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H ≤s G) (X : Set α) : H.deleteVerts X ≤s G.deleteVerts X

theorem Graph.IsClosedSubgraph.deleteVerts {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsClosedSubgraph G) (X : Set α) : (H.deleteVerts X).IsClosedSubgraph (G.deleteVerts X)

theorem Graph.IsClosedSubgraph.deleteVerts_of_disjoint {α : Type u_1} {β : Type u_2} {G H : Graph α β} {X : Set α} (h : H.IsClosedSubgraph G) (hS : Disjoint H.vertexSet X) : H.IsClosedSubgraph (G.deleteVerts X)

theorem Graph.IsClosedSubgraph.diff {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (h₁ : H₁.IsClosedSubgraph G) (h₂ : H₂.IsClosedSubgraph G) : (H₁.deleteVerts H₂.vertexSet).IsClosedSubgraph G

theorem Graph.IsClosedSubgraph.diff_edgeSet {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (h₁ : H₁.IsClosedSubgraph G) (h₂ : H₂.IsClosedSubgraph G) : (H₁.deleteVerts H₂.vertexSet).edgeSet = H₁.edgeSet \ H₂.edgeSet

theorem Graph.IsClosedSubgraph.compl {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsClosedSubgraph G) : (G.deleteVerts H.vertexSet).IsClosedSubgraph G

theorem Graph.IsClosedSubgraph.compl_edgeSet {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsClosedSubgraph G) : (G.deleteVerts H.vertexSet).edgeSet = G.edgeSet \ H.edgeSet

@[simp]

theorem Graph.IsClosedSubgraph.eq_union_deleteVerts {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsClosedSubgraph G) : H ∪ G.deleteVerts H.vertexSet = G

theorem Graph.IsClosedSubgraph.of_deleteEdges_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} {F : Set β} (hclF : H.IsClosedSubgraph (G.deleteEdges F)) : H.IsClosedSubgraph G ↔ G.edgeSet ∩ F ⊆ (G.deleteVerts H.vertexSet).edgeSet

theorem Graph.IsClosedSubgraph.restrict {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsClosedSubgraph G) (F : Set β) : (H.restrict F).IsClosedSubgraph (G.restrict F)

theorem Graph.IsClosedSubgraph.deleteEdges {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsClosedSubgraph G) (F : Set β) : (H.deleteEdges F).IsClosedSubgraph (G.deleteEdges F)