Subgraphs of multigraphs

This file develops the basic theory of subgraphs for multigraphs Graph α β: the subgraph relation, standard classes of subgraphs (spanning, induced, closed), and components.

Main definitions

• H ≤ G: the subgraph relation as a partial order on graphs. This is the preferred spelling over H.IsSubgraph G which it is definitionally equal to.
• H ≤s G (Graph.IsSpanningSubgraph): H has the same vertex set as G.
• H ≤i G (Graph.IsInducedSubgraph): H contains every ambient link between its vertices.
• H ≤c G (Graph.IsClosedSubgraph): H is a union of components of G.

Implementation notes

Following the overall design of Graph, subgraphs are terms of the same type Graph α β rather than a separate Subgraph structure. This allows us to reuse notation and lemmas uniformly and to express the subgraph order directly as a partial order on Graph α β.

G ≤ H is the canonical spelling for "G is a subgraph of H". This is definitionally equal to G.IsSubgraph H which exists only for implementation reasons. The explicit IsSubgraph structure is defined so that stronger subgraph notions (such as IsSpanningSubgraph, IsInducedSubgraph, and IsClosedSubgraph) can extend it. This allows them to inherit fundamental fields and lemmas like vertexSet_mono and edgeSet_mono without lemma duplication. However, in statements and proofs, users use G ≤ H instead. The relation ≤ is the simp normal form, and the API is developed entirely in terms of it.

Tags

graphs, subgraph, induced subgraph, spanning subgraph, closed subgraph

structure Graph.IsSubgraph {α : Type u_1} {β : Type u_2} (H G : Graph α β) : Prop

IsSubgraph H G is NOT the preferred spelling for the subgraph relation. Please use H ≤ G instead.

• vertexSet_mono : H.vertexSet ⊆ G.vertexSet
• isLink_mono ⦃e : β⦄ ⦃x y : α⦄ : H.IsLink e x y → G.IsLink e x y

theorem Graph.isSubgraph_iff {α : Type u_1} {β : Type u_2} (H G : Graph α β) : H.IsSubgraph G ↔ autoParam (H.vertexSet ⊆ G.vertexSet) IsSubgraph.vertexSet_mono._autoParam ∧ autoParam (∀ ⦃e : β⦄ ⦃x y : α⦄, H.IsLink e x y → G.IsLink e x y) IsSubgraph.isLink_mono._autoParam

theorem Graph.IsSubgraph.trans {α : Type u_1} {β : Type u_2} {G G₁ H : Graph α β} (h₁ : H.IsSubgraph G) (h₂ : G.IsSubgraph G₁) : H.IsSubgraph G₁

theorem Graph.IsSubgraph.antisymm {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h₁ : H.IsSubgraph G) (h₂ : G.IsSubgraph H) : H = G

@[implicit_reducible]

instance Graph.instPartialOrder {α : Type u_1} {β : Type u_2} : PartialOrder (Graph α β)

H ≤ G means H is a subgraph of G. It is defined as V(H) ⊆ V(G) and every link of H being a link of G.

Equations

• Graph.instPartialOrder = { le := Graph.IsSubgraph, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[simp]

theorem Graph.isSubgraph_iff_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} : H.IsSubgraph G ↔ H ≤ G

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

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

theorem Graph.IsSubgraph.isLink_iff {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β} (hHG : H ≤ G) (he : e ∈ H.edgeSet) : H.IsLink e x y ↔ G.IsLink e x y

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

theorem Graph.Compatible.of_le_le {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (hH₁G : H₁ ≤ G) (hH₂G : H₂ ≤ G) : H₁.Compatible H₂

Two subgraphs of the same graph are compatible.

theorem Graph.Compatible.of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hHG : H ≤ G) : H.Compatible G

theorem Graph.Compatible.of_ge {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hHG : G ≤ H) : H.Compatible G

theorem Graph.Compatible.anti_left {α : Type u_1} {β : Type u_2} {G G₁ H : Graph α β} (hG₁G : G₁ ≤ G) (h : G.Compatible H) : G₁.Compatible H

theorem Graph.Compatible.anti_right {α : Type u_1} {β : Type u_2} {G H H₁ : Graph α β} (hH₁H : H₁ ≤ H) (h : G.Compatible H) : G.Compatible H₁

theorem Graph.Compatible.anti {α : Type u_1} {β : Type u_2} {G G₁ H H₁ : Graph α β} (hG₁G : G₁ ≤ G) (hH₁H : H₁ ≤ H) (h : G.Compatible H) : G₁.Compatible H₁

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

theorem Graph.IsSubgraph.inc_congr {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} (hHG : H ≤ G) (he : e ∈ H.edgeSet) : H.Inc e x ↔ G.Inc e x

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

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

theorem Graph.IsSubgraph.isLoopAt_congr {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} (hHG : H ≤ G) (he : e ∈ H.edgeSet) : H.IsLoopAt e x ↔ G.IsLoopAt e x

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

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

theorem Graph.IsSubgraph.isNonloopAt_congr {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} (hHG : H ≤ G) (he : e ∈ H.edgeSet) : H.IsNonloopAt e x ↔ G.IsNonloopAt e x

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

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

theorem Graph.le_iff_compatible_subset_subset {α : Type u_1} {β : Type u_2} {G H : Graph α β} : G ≤ H ↔ G.Compatible H ∧ G.vertexSet ⊆ H.vertexSet ∧ G.edgeSet ⊆ H.edgeSet

theorem Graph.Compatible.le_iff {α : Type u_1} {β : Type u_2} {H₁ H₂ : Graph α β} (hH : H₁.Compatible H₂) : H₁ ≤ H₂ ↔ H₁.vertexSet ⊆ H₂.vertexSet ∧ H₁.edgeSet ⊆ H₂.edgeSet

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

theorem Graph.vertexSet_ssubset_or_edgeSet_ssubset_of_lt {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hGH : G < H) : G.vertexSet ⊂ H.vertexSet ∨ G.edgeSet ⊂ H.edgeSet

Spanning Subgraphs

structure Graph.IsSpanningSubgraph {α : Type u_1} {β : Type u_2} (H G : Graph α β) extends H.IsSubgraph G : Prop

H ≤s G (Graph.IsSpanningSubgraph) is a subgraph of G with the same vertex set.

• vertexSet_mono : H.vertexSet ⊆ G.vertexSet
• isLink_mono ⦃e : β⦄ ⦃x y : α⦄ : H.IsLink e x y → G.IsLink e x y
• vertexSet_eq : H.vertexSet = G.vertexSet

theorem Graph.isSpanningSubgraph_iff {α : Type u_1} {β : Type u_2} (H G : Graph α β) : H ≤s G ↔ H.IsSubgraph G ∧ H.vertexSet = G.vertexSet

def Graph.«term_≤s_» : Lean.TrailingParserDescr

H ≤s G (Graph.IsSpanningSubgraph) is a subgraph of G with the same vertex set.

Equations

• Graph.«term_≤s_» = Lean.ParserDescr.trailingNode `Graph.«term_≤s_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤s ") (Lean.ParserDescr.cat `term 51))

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

Alias of Graph.IsSpanningSubgraph.toIsSubgraph.

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

instance Graph.IsSpanningSubgraph.instIsPartialOrder {α : Type u_1} {β : Type u_2} : IsPartialOrder (Graph α β) fun (x1 x2 : Graph α β) => x1 ≤s x2

@[simp]

theorem Graph.IsSpanningSubgraph.rfl {α : Type u_1} {β : Type u_2} {G : Graph α β} : G ≤s G

theorem Graph.IsSpanningSubgraph.anti_right {α : Type u_1} {β : Type u_2} {G H K : Graph α β} (hHK : H ≤ K) (hKG : K ≤ G) (h : H ≤s G) : H ≤s K

theorem Graph.IsSpanningSubgraph.mono_left {α : Type u_1} {β : Type u_2} {G H K : Graph α β} (hHK : H ≤ K) (hKG : K ≤ G) (h : H ≤s G) : K ≤s G

theorem Graph.IsSpanningSubgraph.ext_of_edgeSet {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hE : H.edgeSet = G.edgeSet) (h : H ≤s G) : H = G

Induced Subgraphs

structure Graph.IsInducedSubgraph {α : Type u_1} {β : Type u_2} (H G : Graph α β) extends H.IsSubgraph G : Prop

H ≤i G (Graph.IsInducedSubgraph) is a subgraph of G such that every link of G involving two vertices of H is also a link of H.

• vertexSet_mono : H.vertexSet ⊆ G.vertexSet
• isLink_mono ⦃e : β⦄ ⦃x y : α⦄ : H.IsLink e x y → G.IsLink e x y
• isLink_of_mem_mem ⦃e : β⦄ ⦃x y : α⦄ : G.IsLink e x y → x ∈ H.vertexSet → y ∈ H.vertexSet → H.IsLink e x y

theorem Graph.isInducedSubgraph_iff {α : Type u_1} {β : Type u_2} (H G : Graph α β) : H.IsInducedSubgraph G ↔ H.IsSubgraph G ∧ ∀ ⦃e : β⦄ ⦃x y : α⦄, G.IsLink e x y → x ∈ H.vertexSet → y ∈ H.vertexSet → H.IsLink e x y

def Graph.«term_≤i_» : Lean.TrailingParserDescr

H ≤i G (Graph.IsInducedSubgraph) is a subgraph of G such that every link of G involving two vertices of H is also a link of H.

Equations

• Graph.«term_≤i_» = Lean.ParserDescr.trailingNode `Graph.«term_≤i_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤i ") (Lean.ParserDescr.cat `term 51))

theorem Graph.IsInducedSubgraph.le {α : Type u_1} {β : Type u_2} {H G : Graph α β} (self : H.IsInducedSubgraph G) : H.IsSubgraph G

Alias of Graph.IsInducedSubgraph.toIsSubgraph.

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

instance Graph.IsInducedSubgraph.instIsPartialOrder {α : Type u_1} {β : Type u_2} : IsPartialOrder (Graph α β) fun (x1 x2 : Graph α β) => x1.IsInducedSubgraph x2

@[simp]

theorem Graph.IsInducedSubgraph.rfl {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.IsInducedSubgraph G

theorem Graph.IsInducedSubgraph.isLink_congr {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β} (hx : x ∈ H.vertexSet) (hy : y ∈ H.vertexSet) (h : H.IsInducedSubgraph G) : H.IsLink e x y ↔ G.IsLink e x y

theorem Graph.IsInducedSubgraph.adj_congr {α : Type u_1} {β : Type u_2} {x y : α} {G H : Graph α β} (hx : x ∈ H.vertexSet) (hy : y ∈ H.vertexSet) (h : H.IsInducedSubgraph G) : H.Adj x y ↔ G.Adj x y

theorem Graph.IsInducedSubgraph.anti_right {α : Type u_1} {β : Type u_2} {G H K : Graph α β} (hHK : H ≤ K) (hKG : K ≤ G) (h : H.IsInducedSubgraph G) : H.IsInducedSubgraph K

theorem Graph.IsInducedSubgraph.le_of_le_subset {α : Type u_1} {β : Type u_2} {G H K : Graph α β} (h' : K ≤ G) (hsu : K.vertexSet ⊆ H.vertexSet) (h : H.IsInducedSubgraph G) : K ≤ H

theorem Graph.IsInducedSubgraph.ext_of_vertexSet {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hV : H.vertexSet = G.vertexSet) (h : H.IsInducedSubgraph G) : H = G

theorem Graph.IsSubgraph.not_isInducedSubgraph_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hHG : H ≤ G) : ¬H.IsInducedSubgraph G ↔ ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ H.vertexSet ∧ y ∈ H.vertexSet ∧ e ∉ H.edgeSet

Closed Subgraphs

structure Graph.IsClosedSubgraph {α : Type u_1} {β : Type u_2} (H G : Graph α β) extends H.IsInducedSubgraph G : Prop

H ≤c G (Graph.IsClosedSubgraph) is a union of components of G.

• vertexSet_mono : H.vertexSet ⊆ G.vertexSet
• isLink_mono ⦃e : β⦄ ⦃x y : α⦄ : H.IsLink e x y → G.IsLink e x y
• isLink_of_mem_mem ⦃e : β⦄ ⦃x y : α⦄ : G.IsLink e x y → x ∈ H.vertexSet → y ∈ H.vertexSet → H.IsLink e x y
• closed ⦃e : β⦄ ⦃x : α⦄ : G.Inc e x → x ∈ H.vertexSet → e ∈ H.edgeSet

theorem Graph.isClosedSubgraph_iff {α : Type u_1} {β : Type u_2} (H G : Graph α β) : H.IsClosedSubgraph G ↔ H.IsInducedSubgraph G ∧ ∀ ⦃e : β⦄ ⦃x : α⦄, G.Inc e x → x ∈ H.vertexSet → e ∈ H.edgeSet

def Graph.«term_≤c_» : Lean.TrailingParserDescr

H ≤c G (Graph.IsClosedSubgraph) is a union of components of G.

Equations

• Graph.«term_≤c_» = Lean.ParserDescr.trailingNode `Graph.«term_≤c_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤c ") (Lean.ParserDescr.cat `term 51))

theorem Graph.IsClosedSubgraph.mk' {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hHG : H ≤ G) (hclosed : ∀ ⦃e : β⦄ ⦃x : α⦄, G.Inc e x → x ∈ H.vertexSet → e ∈ H.edgeSet) : H.IsClosedSubgraph G

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

instance Graph.IsClosedSubgraph.instIsPartialOrder {α : Type u_1} {β : Type u_2} : IsPartialOrder (Graph α β) fun (x1 x2 : Graph α β) => x1.IsClosedSubgraph x2

@[simp]

theorem Graph.IsClosedSubgraph.rfl {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.IsClosedSubgraph G

theorem Graph.IsClosedSubgraph.inc_congr {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} (hx : x ∈ H.vertexSet) (hHG : H.IsClosedSubgraph G) : H.Inc e x ↔ G.Inc e x

theorem Graph.IsClosedSubgraph.isLink_congr {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β} (hx : x ∈ H.vertexSet) (hHG : H.IsClosedSubgraph G) : H.IsLink e x y ↔ G.IsLink e x y

theorem Graph.IsClosedSubgraph.mem_iff_of_isLink {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β} (he : G.IsLink e x y) (hHG : H.IsClosedSubgraph G) : x ∈ H.vertexSet ↔ y ∈ H.vertexSet

theorem Graph.IsClosedSubgraph.mem_tfae_of_isLink {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β} (he : G.IsLink e x y) (hHG : H.IsClosedSubgraph G) : [x ∈ H.vertexSet, y ∈ H.vertexSet, e ∈ H.edgeSet].TFAE

theorem Graph.IsClosedSubgraph.adj_congr {α : Type u_1} {β : Type u_2} {x y : α} {G H : Graph α β} (hx : x ∈ H.vertexSet) (hHG : H.IsClosedSubgraph G) : H.Adj x y ↔ G.Adj x y

theorem Graph.IsClosedSubgraph.mem_iff_of_adj {α : Type u_1} {β : Type u_2} {x y : α} {G H : Graph α β} (hxy : G.Adj x y) (hHG : H.IsClosedSubgraph G) : x ∈ H.vertexSet ↔ y ∈ H.vertexSet

theorem Graph.IsClosedSubgraph.anti_right {α : Type u_1} {β : Type u_2} {G G₁ H : Graph α β} (hHG₁ : H ≤ G₁) (hG₁ : G₁ ≤ G) (hHG : H.IsClosedSubgraph G) : H.IsClosedSubgraph G₁

theorem Graph.IsInducedSubgraph.not_isClosedSubgraph_iff_exists_adj {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hHG : H.IsInducedSubgraph G) : ¬H.IsClosedSubgraph G ↔ ∃ (x : α) (y : α), G.Adj x y ∧ x ∈ H.vertexSet ∧ y ∉ H.vertexSet

theorem Graph.IsInducedSubgraph.not_isClosedSubgraph_iff_exists_isLink {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hHG : H.IsInducedSubgraph G) : ¬H.IsClosedSubgraph G ↔ ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ H.vertexSet ∧ y ∉ H.vertexSet