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

theorem Graph.IsLink.of_le_of_mem {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β} (h : G.IsLink e x y) (hle : H ≤ G) (he : e ∈ H.edgeSet) : H.IsLink e x y

theorem Graph.Inc.of_le {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} (h : H.Inc e x) (hle : H ≤ G) : G.Inc e x

theorem Graph.Inc.of_le_of_mem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} (h : G.Inc e x) (hle : H ≤ G) (he : e ∈ H.edgeSet) : H.Inc e x

theorem Graph.IsLoopAt.of_le {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} (h : H.IsLoopAt e x) (hle : H ≤ G) : G.IsLoopAt e x

theorem Graph.IsNonloopAt.of_le {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} (h : H.IsNonloopAt e x) (hle : H ≤ G) : G.IsNonloopAt e x

theorem Graph.Adj.of_le {α : Type u_1} {β : Type u_2} {x y : α} {G H : Graph α β} (h : H.Adj x y) (hle : H ≤ G) : G.Adj x y

theorem Graph.vertexSet_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H ≤ G) : H.vertexSet ⊆ G.vertexSet

theorem Graph.edgeSet_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H ≤ G) : H.edgeSet ⊆ G.edgeSet

@[simp]

theorem Graph.vertexSet_monotone {α : Type u_1} {β : Type u_2} : Monotone vertexSet

@[simp]

theorem Graph.edgeSet_monotone {α : Type u_1} {β : Type u_2} : Monotone edgeSet

theorem Graph.le_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} : H ≤ G ↔ H.vertexSet ⊆ G.vertexSet ∧ ∀ ⦃e : β⦄ ⦃x y : α⦄, H.IsLink e x y → G.IsLink e x y

theorem Graph.isLink_iff_isLink_and_mem_of_le {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β} (hle : H ≤ G) : H.IsLink e x y ↔ G.IsLink e x y ∧ e ∈ H.edgeSet

theorem Graph.le_of_le_le_subset_subset {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (h₁ : H₁ ≤ G) (h₂ : H₂ ≤ G) (hV : H₁.vertexSet ⊆ H₂.vertexSet) (hE : H₁.edgeSet ⊆ H₂.edgeSet) : H₁ ≤ H₂

theorem Graph.ext_of_le_le {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (h₁ : H₁ ≤ G) (h₂ : H₂ ≤ G) (hV : H₁.vertexSet = H₂.vertexSet) (hE : H₁.edgeSet = H₂.edgeSet) : H₁ = H₂

theorem Graph.eq_of_le_of_edgeSet_subset_of_isolated {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hle : H ≤ G) (hE : G.edgeSet ⊆ H.edgeSet) (hV : ∀ ⦃v : α⦄, G.Isolated v → v ∈ H.vertexSet) : H = G

If H is a subgraph of G containing all edges and isolated vertices of G, then H = G

theorem Graph.le_of_le_le_edgeSet_subset_of_isolated {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (h₁ : H₁ ≤ G) (h₂ : H₂ ≤ G) (hE : H₁.edgeSet ⊆ H₂.edgeSet) (hV : ∀ ⦃v : α⦄, H₁.Isolated v → v ∈ H₂.vertexSet) : H₁ ≤ H₂

theorem Graph.ext_of_le_le_of_isolated {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (h₁ : H₁ ≤ G) (h₂ : H₂ ≤ G) (hE : H₁.edgeSet = H₂.edgeSet) (h : H₁.IsolatedSet = H₂.IsolatedSet) : H₁ = H₂

theorem Graph.isLink_eq_of_le {α : Type u_1} {β : Type u_2} {e : β} {G H : Graph α β} (hle : H ≤ G) (he : e ∈ H.edgeSet) : H.IsLink e = G.IsLink e

theorem Graph.isLink_eqOn_of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hle : H ≤ G) : Set.EqOn H.IsLink G.IsLink H.edgeSet

theorem Graph.inc_eq_of_le {α : Type u_1} {β : Type u_2} {e : β} {G H : Graph α β} (hle : H ≤ G) (he : e ∈ H.edgeSet) : H.Inc e = G.Inc e

theorem Graph.inc_eqOn_of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hle : H ≤ G) : Set.EqOn H.Inc G.Inc H.edgeSet

theorem Graph.isLoopAt_eq_of_le {α : Type u_1} {β : Type u_2} {e : β} {G H : Graph α β} (hle : H ≤ G) (he : e ∈ H.edgeSet) : H.IsLoopAt e = G.IsLoopAt e

theorem Graph.isLoopAt_eqOn_of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hle : H ≤ G) : Set.EqOn H.IsLoopAt G.IsLoopAt H.edgeSet

theorem Graph.isNonloopAt_eq_of_le {α : Type u_1} {β : Type u_2} {e : β} {G H : Graph α β} (hle : H ≤ G) (he : e ∈ H.edgeSet) : H.IsNonloopAt e = G.IsNonloopAt e

theorem Graph.isNonloopAt_eqOn_of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hle : H ≤ G) : Set.EqOn H.IsNonloopAt G.IsNonloopAt H.edgeSet

theorem Graph.lt_of_le_of_vertexSet_ssubset {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hle : G ≤ H) (h : G.vertexSet ⊂ H.vertexSet) : G < H

theorem Graph.lt_of_le_of_edgeSet_ssubset {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hle : G ≤ H) (h : G.edgeSet ⊂ H.edgeSet) : G < H

theorem Graph.exists_edge_or_vertex_of_lt {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G < H) : (∃ e ∈ H.edgeSet, e ∉ G.edgeSet) ∨ ∃ v ∈ H.vertexSet, v ∉ G.vertexSet

theorem Graph.sum_ncard_lt_of_lt {α : Type u_1} {β : Type u_2} {G H : Graph α β} [Finite α] [Finite β] (h : G < H) : G.vertexSet.ncard + G.edgeSet.ncard < H.vertexSet.ncard + H.edgeSet.ncard

theorem Graph.neighbor_mono {α : Type u_1} {β : Type u_2} {x : α} {G H : Graph α β} (hle : G ≤ H) : N(G, x) ⊆ N(H, x)

theorem Graph.setNeighbor_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hle : G ≤ H) (S : Set α) : N(G, S) ⊆ N(H, S)

theorem Graph.incEdges_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hle : G ≤ H) (x : α) : E(G, x) ⊆ E(H, x)

theorem Graph.setIncEdges_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hle : G ≤ H) (S : Set α) : E(G, S) ⊆ E(H, S)

theorem Graph.endSet_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hle : G ≤ H) (e : β) : V(G, e) ⊆ V(H, e)

@[simp]

theorem Graph.endSet_eq_of_le {α : Type u_1} {β : Type u_2} {e : β} {G H : Graph α β} (hle : G ≤ H) (he : e ∈ G.edgeSet) : V(H, e) = V(G, e)

theorem Graph.incVertexSet_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hle : G ≤ H) (F : Set β) : V(G, F) ⊆ V(H, F)

theorem Graph.incVertexSet_subset_of_subset_of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} {F : Set β} (hle : G ≤ H) (hF : F ⊆ G.edgeSet) : V(H, F) ⊆ G.vertexSet

theorem Graph.linkEdges_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hle : G ≤ H) (u v : α) : E(G, u, v) ⊆ E(H, u, v)

theorem Graph.setLinkEdges_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hle : G ≤ H) (S T : Set α) : E(G, S, T) ⊆ E(H, S, T)

theorem Graph.setLinkEdges_eq_inter_of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hle : G ≤ H) (S T : Set α) : E(G, S, T) = G.edgeSet ∩ E(H, S, T)

theorem Graph.setLinkEdges_eq_inter_of_le' {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hle : G ≤ H) (S : Set α) : E(G, S, G.vertexSet \ S) = G.edgeSet ∩ E(H, S, H.vertexSet \ S)

instance Graph.instWellFoundedLTOfFinite_matroid {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] : WellFoundedLT (Graph α β)

Spanning Subgraphs

theorem Graph.IsSpanningSubgraph.mk' {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hV : H.vertexSet = G.vertexSet) (hl : ∀ ⦃e : β⦄ ⦃x y : α⦄, H.IsLink e x y → G.IsLink e x y) : H ≤s G

theorem Graph.IsSpanningSubgraph.le' {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H ≤s G) : H ≤ G

@[simp]

theorem Graph.bot_isSpanningSubgraph_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : ⊥ ≤s G ↔ G = ⊥

Induced Subgraphs

theorem Graph.IsInducedSubgraph.le' {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsInducedSubgraph G) : H ≤ G

Closed Subgraphs

theorem Graph.IsClosedSubgraph.le' {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsClosedSubgraph G) : H ≤ G

theorem Graph.isClosedSubgraph_iff_le_and_setLinkEdges_empty {α : Type u_1} {β : Type u_2} {G H : Graph α β} : H.IsClosedSubgraph G ↔ H.IsInducedSubgraph G ∧ E(G, H.vertexSet, G.vertexSet \ H.vertexSet) = ∅

theorem Graph.IsClosedSubgraph.setLinkEdges_empty {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsClosedSubgraph G) : E(G, H.vertexSet, G.vertexSet \ H.vertexSet) = ∅

theorem Graph.IsClosedSubgraph.adj_of_adj_of_mem {α : Type u_1} {β : Type u_2} {x y : α} {G H : Graph α β} (h : H.IsClosedSubgraph G) (hx : x ∈ H.vertexSet) (hxy : G.Adj x y) : H.Adj x y

Components

def Graph.IsCompOf {α : Type u_1} {β : Type u_2} (H G : Graph α β) : Prop

A component of G is a minimal nonempty closed subgraph of G.

Equations

• H.IsCompOf G = Minimal (fun (H : Graph α β) => H.IsClosedSubgraph G ∧ H.vertexSet.Nonempty) H

@[simp]

theorem Graph.IsCompOf.isClosedSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsCompOf G) : H.IsClosedSubgraph G

@[simp]

theorem Graph.IsCompOf.isInducedSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hHco : H.IsCompOf G) : H.IsInducedSubgraph G

@[simp]

theorem Graph.IsCompOf.le {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsCompOf G) : H ≤ G

@[simp]

theorem Graph.IsCompOf.nonempty {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsCompOf G) : H.vertexSet.Nonempty

theorem Graph.IsCompOf.subset {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsCompOf G) : H.vertexSet ⊆ G.vertexSet

instance Graph.instvxNonemptyOfEdgeNonempty {α : Type u_1} {β : Type u_2} (G : Graph α β) [hE : Nonempty ↑G.edgeSet] : Nonempty ↑G.vertexSet