Matroid.Graph.Constructions.Sum

source

theorem Graph.stronglyDisjoint_map_inl_map_inr {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} :

((map Sum.inl G₁).edgeMap Sum.inl ⋯).StronglyDisjoint ((map Sum.inr G₂).edgeMap Sum.inr ⋯)

source

def Graph.directSum {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} (G₁ : Graph α₁ β₁) (G₂ : Graph α₂ β₂) :

Graph (α₁ ⊕ α₂) (β₁ ⊕ β₂)

The direct sum of graphs with arbitrary vertex and edge types. TODO : direct sigma .

Equations

G₁.directSum G₂ = ((Graph.map Sum.inl G₁).edgeMap Sum.inl ⋯ ∪ (Graph.map Sum.inr G₂).edgeMap Sum.inr ⋯).copy ⋯ ⋯ ⋯

Instances For

source

@[simp]

theorem Graph.edgeSet_directSum {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} (G₁ : Graph α₁ β₁) (G₂ : Graph α₂ β₂) :

(G₁.directSum G₂).edgeSet = Sum.inl '' G₁.edgeSet ∪ Sum.inr '' G₂.edgeSet

source

@[simp]

theorem Graph.vertexSet_directSum {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} (G₁ : Graph α₁ β₁) (G₂ : Graph α₂ β₂) :

(G₁.directSum G₂).vertexSet = Sum.inl '' G₁.vertexSet ∪ Sum.inr '' G₂.vertexSet

source

theorem Graph.directSum_isLink_eq_match {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} :

(G₁.directSum G₂).IsLink = fun (e : β₁ ⊕ β₂) (x y : α₁ ⊕ α₂) => match e, x, y with | Sum.inl e, Sum.inl x, Sum.inl y => G₁.IsLink e x y | Sum.inr e, Sum.inr x, Sum.inr y => G₂.IsLink e x y | x, x_1, x_2 => False

source

theorem Graph.directSum_inc_eq_match {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} :

(G₁.directSum G₂).Inc = fun (e : β₁ ⊕ β₂) (x : α₁ ⊕ α₂) => match e, x with | Sum.inl e, Sum.inl x => G₁.Inc e x | Sum.inr e, Sum.inr x => G₂.Inc e x | x, x_1 => False

source

theorem Graph.directSum_isLink_inl_inl_iff_exists {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} {e : β₁ ⊕ β₂} {x y : α₁} :

(G₁.directSum G₂).IsLink e (Sum.inl x) (Sum.inl y) ↔ ∃ (e₀ : β₁), e = Sum.inl e₀ ∧ G₁.IsLink e₀ x y

source

theorem Graph.directSum_isLink_inl_iff_exists {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} {e : β₁} {x y : α₁ ⊕ α₂} :

(G₁.directSum G₂).IsLink (Sum.inl e) x y ↔ ∃ (x₀ : α₁) (y₀ : α₁), G₁.IsLink e x₀ y₀ ∧ x = Sum.inl x₀ ∧ y = Sum.inl y₀

source

theorem Graph.directSum_isLink_inr_iff_exists {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} {e : β₂} {x y : α₁ ⊕ α₂} :

(G₁.directSum G₂).IsLink (Sum.inr e) x y ↔ ∃ (x₀ : α₂) (y₀ : α₂), G₂.IsLink e x₀ y₀ ∧ x = Sum.inr x₀ ∧ y = Sum.inr y₀

source

@[simp]

theorem Graph.directSum_not_isLink_inl_inr_right {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} {e : β₁} {x : α₁ ⊕ α₂} {y : α₂} :

¬(G₁.directSum G₂).IsLink (Sum.inl e) x (Sum.inr y)

source

@[simp]

theorem Graph.directSum_not_isLink_inl_inr_left {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} {e : β₁} {x : α₂} {y : α₁ ⊕ α₂} :

¬(G₁.directSum G₂).IsLink (Sum.inl e) (Sum.inr x) y

source

@[simp]

theorem Graph.directSum_not_isLink_inr_inl_right {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} {e : β₂} {x : α₁ ⊕ α₂} {y : α₁} :

¬(G₁.directSum G₂).IsLink (Sum.inr e) x (Sum.inl y)

source

@[simp]

theorem Graph.directSum_not_isLink_inr_inl_left {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} {e : β₂} {x : α₁} {y : α₁ ⊕ α₂} :

¬(G₁.directSum G₂).IsLink (Sum.inr e) (Sum.inl x) y

source

@[simp]

theorem Graph.directSum_not_isLink_inl_inr {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} {e : β₁ ⊕ β₂} {x : α₁} {y : α₂} :

¬(G₁.directSum G₂).IsLink e (Sum.inl x) (Sum.inr y)

source

@[simp]

theorem Graph.directSum_not_isLink_inr_inl {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} {e : β₁ ⊕ β₂} {x : α₂} {y : α₁} :

¬(G₁.directSum G₂).IsLink e (Sum.inr x) (Sum.inl y)

source

@[simp]

theorem Graph.directSum_isLink_inl_inl_inl_iff {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} {e : β₁} {x y : α₁} :

(G₁.directSum G₂).IsLink (Sum.inl e) (Sum.inl x) (Sum.inl y) ↔ G₁.IsLink e x y

source

@[simp]

theorem Graph.directSum_isLink_inr_inr_inr_iff {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} {e : β₂} {x y : α₂} :

(G₁.directSum G₂).IsLink (Sum.inr e) (Sum.inr x) (Sum.inr y) ↔ G₂.IsLink e x y

source

theorem Graph.directSum_inc_iff {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} {e : β₁ ⊕ β₂} {x : α₁ ⊕ α₂} :

(G₁.directSum G₂).Inc e x ↔ (∃ (e₀ : β₁) (x₀ : α₁), G₁.Inc e₀ x₀ ∧ e = Sum.inl e₀ ∧ x = Sum.inl x₀) ∨ ∃ (e₀ : β₂) (x₀ : α₂), G₂.Inc e₀ x₀ ∧ e = Sum.inr e₀ ∧ x = Sum.inr x₀

source

theorem Graph.directSum_inc_inl_iff {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} {e : β₁} {x : α₁ ⊕ α₂} :

(G₁.directSum G₂).Inc (Sum.inl e) x ↔ ∃ (x₀ : α₁), G₁.Inc e x₀ ∧ x = Sum.inl x₀

source

theorem Graph.directSum_inc_inr_iff {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} {e : β₂} {x : α₁ ⊕ α₂} :

(G₁.directSum G₂).Inc (Sum.inr e) x ↔ ∃ (x₀ : α₂), G₂.Inc e x₀ ∧ x = Sum.inr x₀

source

@[simp]

theorem Graph.directSum_not_inc_inl_inr {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} {e : β₁} {x : α₂} :

¬(G₁.directSum G₂).Inc (Sum.inl e) (Sum.inr x)

source

@[simp]

theorem Graph.directSum_inc_inl_inl_iff {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} {e : β₁} {x : α₁} :

(G₁.directSum G₂).Inc (Sum.inl e) (Sum.inl x) ↔ G₁.Inc e x

source

@[simp]

theorem Graph.directSum_inc_inr_inr_iff {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} {e : β₂} {x : α₂} :

(G₁.directSum G₂).Inc (Sum.inr e) (Sum.inr x) ↔ G₂.Inc e x

source

@[simp]

theorem Graph.directSum_adj_inl_inl_iff {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} {x y : α₁} :

(G₁.directSum G₂).Adj (Sum.inl x) (Sum.inl y) ↔ G₁.Adj x y

source

@[simp]

theorem Graph.directSum_adj_inr_inr_iff {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} {x y : α₂} :

(G₁.directSum G₂).Adj (Sum.inr x) (Sum.inr y) ↔ G₂.Adj x y

source

@[simp]

theorem Graph.directSum_not_adj_inr_inl {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} {x : α₂} {y : α₁} :

¬(G₁.directSum G₂).Adj (Sum.inr x) (Sum.inl y)

source

@[simp]

theorem Graph.directSum_not_adj_inl_inr {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} {x : α₁} {y : α₂} :

¬(G₁.directSum G₂).Adj (Sum.inl x) (Sum.inr y)

source

theorem Graph.directSum_isLoopAt_iff {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} {e : β₁ ⊕ β₂} {x : α₁ ⊕ α₂} :

(G₁.directSum G₂).IsLoopAt e x ↔ (∃ (e₀ : β₁) (x₀ : α₁), G₁.IsLoopAt e₀ x₀ ∧ e = Sum.inl e₀ ∧ x = Sum.inl x₀) ∨ ∃ (e₀ : β₂) (x₀ : α₂), G₂.IsLoopAt e₀ x₀ ∧ e = Sum.inr e₀ ∧ x = Sum.inr x₀

source

theorem Graph.directSum_isNonLoopAt_iff {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} {e : β₁ ⊕ β₂} {x : α₁ ⊕ α₂} :

(G₁.directSum G₂).IsNonloopAt e x ↔ (∃ (e₀ : β₁) (x₀ : α₁), G₁.IsNonloopAt e₀ x₀ ∧ e = Sum.inl e₀ ∧ x = Sum.inl x₀) ∨ ∃ (e₀ : β₂) (x₀ : α₂), G₂.IsNonloopAt e₀ x₀ ∧ e = Sum.inr e₀ ∧ x = Sum.inr x₀

source

@[simp]

theorem Graph.directSum_loopless_iff {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} :

(G₁.directSum G₂).Loopless ↔ G₁.Loopless ∧ G₂.Loopless

source

@[simp]

theorem Graph.directSum_simple_iff {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} :

(G₁.directSum G₂).Simple ↔ G₁.Simple ∧ G₂.Simple

source

instance Graph.Loopless.directSum_loopless {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} [hG₁ : G₁.Loopless] [hG₂ : G₂.Loopless] :

(G₁.directSum G₂).Loopless

source

instance Graph.Simple.directSum_simple {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} [hG₁ : G₁.Simple] [hG₂ : G₂.Simple] :

(G₁.directSum G₂).Simple

source

theorem Graph.directSum_deleteVerts {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} (G₁ : Graph α₁ β₁) (G₂ : Graph α₂ β₂) (X : Set (α₁ ⊕ α₂)) :

(G₁.directSum G₂).deleteVerts X = (G₁.deleteVerts (Sum.inl ⁻¹' X)).directSum (G₂.deleteVerts (Sum.inr ⁻¹' X))

source

theorem Graph.directSum_deleteVerts_left {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} (G₁ : Graph α₁ β₁) (G₂ : Graph α₂ β₂) (X : Set α₁) :

(G₁.directSum G₂).deleteVerts (Sum.inl '' X) = (G₁.deleteVerts X).directSum G₂

source

theorem Graph.directSum_deleteVerts_right {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} (G₁ : Graph α₁ β₁) (G₂ : Graph α₂ β₂) (X : Set α₂) :

(G₁.directSum G₂).deleteVerts (Sum.inr '' X) = G₁.directSum (G₂.deleteVerts X)

source

theorem Graph.directSum_map_swap {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} (G₁ : Graph α₁ β₁) (G₂ : Graph α₂ β₂) :

(map Sum.swap (G₁.directSum G₂)).edgeMap Sum.swap ⋯ = G₂.directSum G₁

source

@[simp]

theorem Graph.bot_directSum {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} (G₂ : Graph α₂ β₂) :

⊥.directSum G₂ = (map Sum.inr G₂).edgeMap Sum.inr ⋯

source

@[simp]

theorem Graph.directSum_bot {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} (G₁ : Graph α₁ β₁) :

G₁.directSum ⊥ = (map Sum.inl G₁).edgeMap Sum.inl ⋯

source

theorem Graph.directSum_map {α : Type u_1} {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} (G₁ : Graph α₁ β₁) (G₂ : Graph α₂ β₂) {φ : α₁ ⊕ α₂ → α} :

map φ (G₁.directSum G₂) = map (Sum.elim id id) ((map (φ ∘ Sum.inl) G₁).directSum (map (φ ∘ Sum.inr) G₂))

source

theorem Graph.directSum_map_left {α : Type u_1} {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} (G₁ : Graph α₁ β₁) (G₂ : Graph α₂ β₂) {φ : α₁ → α} :

(map φ G₁).directSum G₂ = map (Sum.map φ id) (G₁.directSum G₂)

source

theorem Graph.directSum_map_right {α : Type u_1} {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} (G₁ : Graph α₁ β₁) (G₂ : Graph α₂ β₂) {φ : α₂ → α} :

G₁.directSum (map φ G₂) = map (Sum.map id φ) (G₁.directSum G₂)

source

@[simp]

theorem Graph.directSum_eq_bot_iff {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} :

G₁.directSum G₂ = ⊥ ↔ G₁ = ⊥ ∧ G₂ = ⊥

source

theorem Graph.directSum_connected_iff {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} :

(G₁.directSum G₂).Connected ↔ G₁ = ⊥ ∧ G₂.Connected ∨ G₁.Connected ∧ G₂ = ⊥

source

theorem Graph.directSum_preconnected_iff {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} :

(G₁.directSum G₂).Preconnected ↔ G₁ = ⊥ ∧ G₂.Preconnected ∨ G₁.Preconnected ∧ G₂ = ⊥

source

theorem Graph.directSum_isComplete_iff {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} {G₁ : Graph α₁ β₁} {G₂ : Graph α₂ β₂} :

(G₁.directSum G₂).IsComplete ↔ G₁.IsComplete ∧ G₂ = ⊥ ∨ G₁ = ⊥ ∧ G₂.IsComplete

source

theorem Graph.directSum_eDegree_inl {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} (G₁ : Graph α₁ β₁) (G₂ : Graph α₂ β₂) (x : α₁) :

(G₁.directSum G₂).eDegree (Sum.inl x) = G₁.eDegree x

source

theorem Graph.directSum_eDegree_inr {α₁ : Type u_10} {α₂ : Type u_11} {β₁ : Type u_12} {β₂ : Type u_13} (G₁ : Graph α₁ β₁) (G₂ : Graph α₂ β₂) (x : α₂) :

(G₁.directSum G₂).eDegree (Sum.inr x) = G₂.eDegree x

source

def Graph.directEdgeSum {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} (G₁ : Graph α β₁) (G₂ : Graph α β₂) :

Graph α (β₁ ⊕ β₂)

The edge-union of two graphs with the same vertex type, where the edge type is a sum.

Equations

G₁.directEdgeSum G₂ = (G₁.edgeMap Sum.inl ⋯ ∪ G₂.edgeMap Sum.inr ⋯).copy ⋯ ⋯ ⋯

Instances For

source

@[simp]

theorem Graph.vertexSet_directEdgeSum {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} (G₁ : Graph α β₁) (G₂ : Graph α β₂) :

(G₁.directEdgeSum G₂).vertexSet = G₁.vertexSet ∪ G₂.vertexSet

source

@[simp]

theorem Graph.edgeSet_directEdgeSum {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} (G₁ : Graph α β₁) (G₂ : Graph α β₂) :

(G₁.directEdgeSum G₂).edgeSet = Sum.inl '' G₁.edgeSet ∪ Sum.inr '' G₂.edgeSet

source

theorem Graph.directEdgeSum_isLink_eq_match {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} (G₁ : Graph α β₁) (G₂ : Graph α β₂) :

(G₁.directEdgeSum G₂).IsLink = fun (e : β₁ ⊕ β₂) (x y : α) => match e, x, y with | Sum.inl e, x, y => G₁.IsLink e x y | Sum.inr e, x, y => G₂.IsLink e x y

source

@[simp]

theorem Graph.directEdgeSum_isLink_inl_iff {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} {G₁ : Graph α β₁} {G₂ : Graph α β₂} {e : β₁} {x y : α} :

(G₁.directEdgeSum G₂).IsLink (Sum.inl e) x y ↔ G₁.IsLink e x y

source

@[simp]

theorem Graph.directEdgeSum_isLink_inr_iff {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} {G₁ : Graph α β₁} {G₂ : Graph α β₂} {e : β₂} {x y : α} :

(G₁.directEdgeSum G₂).IsLink (Sum.inr e) x y ↔ G₂.IsLink e x y

source

@[simp]

theorem Graph.directEdgeSum_inc_inl_iff {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} {G₁ : Graph α β₁} {G₂ : Graph α β₂} {e : β₁} {x : α} :

(G₁.directEdgeSum G₂).Inc (Sum.inl e) x ↔ G₁.Inc e x

source

@[simp]

theorem Graph.directEdgeSum_inc_inr_iff {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} {G₁ : Graph α β₁} {G₂ : Graph α β₂} {e : β₂} {x : α} :

(G₁.directEdgeSum G₂).Inc (Sum.inr e) x ↔ G₂.Inc e x

source

@[simp]

theorem Graph.directEdgeSum_adj_iff {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} {G₁ : Graph α β₁} {G₂ : Graph α β₂} {x y : α} :

(G₁.directEdgeSum G₂).Adj x y ↔ G₁.Adj x y ∨ G₂.Adj x y

source

@[simp]

theorem Graph.directEdgeSum_isNonloopAt_inl_iff {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} {G₁ : Graph α β₁} {G₂ : Graph α β₂} {e : β₁} {x : α} :

(G₁.directEdgeSum G₂).IsNonloopAt (Sum.inl e) x ↔ G₁.IsNonloopAt e x

source

@[simp]

theorem Graph.directEdgeSum_isNonloopAt_inr_iff {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} {G₁ : Graph α β₁} {G₂ : Graph α β₂} {e : β₂} {x : α} :

(G₁.directEdgeSum G₂).IsNonloopAt (Sum.inr e) x ↔ G₂.IsNonloopAt e x

source

@[simp]

theorem Graph.directEdgeSum_isLoopAt_inl_iff {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} {G₁ : Graph α β₁} {G₂ : Graph α β₂} {e : β₁} {x : α} :

(G₁.directEdgeSum G₂).IsLoopAt (Sum.inl e) x ↔ G₁.IsLoopAt e x

source

@[simp]

theorem Graph.directEdgeSum_isLoopAt_inr_iff {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} {G₁ : Graph α β₁} {G₂ : Graph α β₂} {e : β₂} {x : α} :

(G₁.directEdgeSum G₂).IsLoopAt (Sum.inr e) x ↔ G₂.IsLoopAt e x

source

theorem Graph.directEdgeSum_comm {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} (G₁ : Graph α β₁) (G₂ : Graph α β₂) :

G₁.directEdgeSum G₂ = (G₂.directEdgeSum G₁).edgeMap Sum.swap ⋯

source

@[simp]

theorem Graph.directSum_map_elim {α : Type u_1} {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_10} {β₂ : Type u_11} (G₁ : Graph α₁ β₁) (G₂ : Graph α₂ β₂) {φ₁ : α₁ → α} {φ₂ : α₂ → α} :

map (Sum.elim φ₁ φ₂) (G₁.directSum G₂) = (map φ₁ G₁).directEdgeSum (map φ₂ G₂)

source

@[simp]

theorem Graph.directEdgeSum_eDegree {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} (G₁ : Graph α β₁) (G₂ : Graph α β₂) (x : α) :

(G₁.directEdgeSum G₂).eDegree x = G₁.eDegree x + G₂.eDegree x

source

@[simp]

theorem Graph.directEdgeSum_loopless_iff {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} {G₁ : Graph α β₁} {G₂ : Graph α β₂} :

(G₁.directEdgeSum G₂).Loopless ↔ G₁.Loopless ∧ G₂.Loopless

source

@[simp]

theorem Graph.directEdgeSum_deleteVerts {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} (G₁ : Graph α β₁) (G₂ : Graph α β₂) (X : Set α) :

(G₁.directEdgeSum G₂).deleteVerts X = (G₁.deleteVerts X).directEdgeSum (G₂.deleteVerts X)

source

theorem Graph.directEdgeSum_simple_iff {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} {G₁ : Graph α β₁} {G₂ : Graph α β₂} :

(G₁.directEdgeSum G₂).Simple ↔ G₁.Simple ∧ G₂.Simple ∧ ∀ (x y : α), ¬(G₁.Adj x y ∧ G₂.Adj x y)

source

theorem Graph.directEdgeSum_isComplete_iff {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} {G₁ : Graph α β₁} {G₂ : Graph α β₂} :

(G₁.directEdgeSum G₂).IsComplete ↔ ∀ (x y : α), x ∈ G₁.vertexSet ∪ G₂.vertexSet → y ∈ G₁.vertexSet ∪ G₂.vertexSet → x ≠ y → G₁.Adj x y ∨ G₂.Adj x y

source

@[simp]

theorem Graph.directEdgeSum_noEdge_right {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} (G₁ : Graph α β₁) (V : Set α) :

G₁.directEdgeSum (noEdge V β₂) = (G₁.edgeMap Sum.inl ⋯)[G₁.vertexSet ∪ V]

source

@[simp]

theorem Graph.directEdgeSum_noEdge_left {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} (G₂ : Graph α β₂) (V : Set α) :

(noEdge V β₁).directEdgeSum G₂ = (G₂.edgeMap Sum.inr ⋯)[G₂.vertexSet ∪ V]

source

theorem Graph.le_directEdgeSum_left {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} (G₁ : Graph α β₁) (G₂ : Graph α β₂) :

G₁.edgeMap Sum.inl ⋯ ≤ G₁.directEdgeSum G₂

source

theorem Graph.le_directEdgeSum_right {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} (G₁ : Graph α β₁) (G₂ : Graph α β₂) :

G₂.edgeMap Sum.inr ⋯ ≤ G₁.directEdgeSum G₂

source

theorem Graph.isSpanningSubgraph_directEdgeSum_left {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} {G₁ : Graph α β₁} {G₂ : Graph α β₂} (hG : G₂.vertexSet ⊆ G₁.vertexSet) :

G₁.edgeMap Sum.inl ⋯ ≤s G₁.directEdgeSum G₂

source

theorem Graph.isSpanningSubgraph_directEdgeSum_right {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} {G₁ : Graph α β₁} {G₂ : Graph α β₂} (hG : G₁.vertexSet ⊆ G₂.vertexSet) :

G₂.edgeMap Sum.inr ⋯ ≤s G₁.directEdgeSum G₂

source

theorem Graph.Preconnected.directEdgeSum_preconnected_right {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} {G₁ : Graph α β₁} {G₂ : Graph α β₂} (hG₁ : G₁.Preconnected) (hG₂ : G₂.vertexSet ⊆ G₁.vertexSet) :

(G₁.directEdgeSum G₂).Preconnected

source

theorem Graph.Preconnected.directEdgeSum_preconnected_left {α : Type u_1} {β₁ : Type u_10} {β₂ : Type u_11} {G₁ : Graph α β₁} {G₂ : Graph α β₂} (hG₂ : G₂.Preconnected) (hG₁ : G₁.vertexSet ⊆ G₂.vertexSet) :

(G₁.directEdgeSum G₂).Preconnected

source

def Graph.multiApex {α : Type u_1} {β : Type u_3} {γ : Type u_10} (G : Graph α β) (A : Set γ) :

Graph (α ⊕ γ) (β ⊕ α × γ)

Equations

G.multiApex A = ((G.directSum (Graph.noEdge A Empty)).edgeMap (Sum.elim id Empty.elim) ⋯).directEdgeSum (Graph.completeBipartiteGraphOn G.vertexSet A)

Instances For

source

@[simp]

theorem Graph.multiApex_vertexSet {α : Type u_1} {β : Type u_3} {γ : Type u_10} (G : Graph α β) (A : Set γ) :

(G.multiApex A).vertexSet = Sum.inl '' G.vertexSet ∪ Sum.inr '' A

source

@[simp]

theorem Graph.multiApex_edgeSet {α : Type u_1} {β : Type u_3} {γ : Type u_10} (G : Graph α β) (A : Set γ) :

(G.multiApex A).edgeSet = Sum.inl '' G.edgeSet ∪ Sum.inr '' G.vertexSet ×ˢ A

source

theorem Graph.multiApex_isLink_eq_match {α : Type u_1} {β : Type u_3} {G : Graph α β} {γ : Type u_10} {A : Set γ} :

(G.multiApex A).IsLink = fun (e : β ⊕ α × γ) (x y : α ⊕ γ) => match e, x, y with | Sum.inl e, Sum.inl x, Sum.inl y => G.IsLink e x y | Sum.inr (u, a), Sum.inl x, Sum.inr y => u ∈ G.vertexSet ∧ a ∈ A ∧ x = u ∧ y = a | Sum.inr (u, a), Sum.inr x, Sum.inl y => u ∈ G.vertexSet ∧ a ∈ A ∧ y = u ∧ x = a | x, x_1, x_2 => False

source

theorem Graph.multiApex_isLink_inl_eq_match {α : Type u_1} {β : Type u_3} {G : Graph α β} {γ : Type u_10} {A : Set γ} {e : β} {x y : α ⊕ γ} :

(G.multiApex A).IsLink (Sum.inl e) x y ↔ match x, y with | Sum.inl x, Sum.inl y => G.IsLink e x y | x, x_1 => false = true

source

theorem Graph.multiApex_isLink_inr_eq_match {α : Type u_1} {β : Type u_3} {G : Graph α β} {γ : Type u_10} {A : Set γ} {e : α × γ} {x y : α ⊕ γ} :

(G.multiApex A).IsLink (Sum.inr e) x y ↔ match x, y with | Sum.inl x, Sum.inr y => e.1 ∈ G.vertexSet ∧ e.2 ∈ A ∧ x = e.1 ∧ y = e.2 | Sum.inr x, Sum.inl y => e.1 ∈ G.vertexSet ∧ e.2 ∈ A ∧ x = e.2 ∧ y = e.1 | x, x_1 => False

source

theorem Graph.multiApex_inc_eq {α : Type u_1} {β : Type u_3} {G : Graph α β} {γ : Type u_10} {A : Set γ} :

(G.multiApex A).Inc = fun (e : β ⊕ α × γ) (x : α ⊕ γ) => match e, x with | Sum.inl e, Sum.inl x => G.Inc e x | Sum.inr (u, a), Sum.inl x => u ∈ G.vertexSet ∧ a ∈ A ∧ x = u | Sum.inr (u, a), Sum.inr x => u ∈ G.vertexSet ∧ a ∈ A ∧ x = a | x, x_1 => False

source

@[simp]

theorem Graph.multiApex_loopless_iff {α : Type u_1} {β : Type u_3} {G : Graph α β} {γ : Type u_10} {A : Set γ} :

(G.multiApex A).Loopless ↔ G.Loopless

source

@[simp]

theorem Graph.multiApex_simple_iff {α : Type u_1} {β : Type u_3} {G : Graph α β} {γ : Type u_10} {A : Set γ} :

(G.multiApex A).Simple ↔ G.Simple

source

@[simp]

theorem Graph.multiApex_empty {α : Type u_1} {β : Type u_3} {G : Graph α β} {γ : Type u_10} :

G.multiApex ∅ = (map Sum.inl G).edgeMap Sum.inl ⋯

source

theorem Graph.multiApex_preconnected_iff {α : Type u_1} {β : Type u_3} {G : Graph α β} {γ : Type u_10} {A : Set γ} :

(G.multiApex A).Preconnected ↔ (G = ⊥ → A.Subsingleton) ∧ (A = ∅ → G.Preconnected)

source

theorem Graph.multiApex_connected_iff {α : Type u_1} {β : Type u_3} {G : Graph α β} {γ : Type u_10} {A : Set γ} :

(G.multiApex A).Connected ↔ (A = ∅ → G.Connected) ∧ (G = ⊥ → A.Subsingleton)

source

@[simp]

theorem Graph.multiApex_isComplete_iff {α : Type u_1} {β : Type u_3} {G : Graph α β} {γ : Type u_10} {A : Set γ} :

(G.multiApex A).IsComplete ↔ G.IsComplete ∧ A.Subsingleton

source

theorem Graph.multiApex_deleteVerts_left {α : Type u_1} {β : Type u_3} {γ : Type u_10} {A : Set γ} (G : Graph α β) (X : Set α) :

(G.deleteVerts X).multiApex A = (G.multiApex A).deleteVerts (Sum.inl '' X)

source

theorem Graph.multiApex_sdiff_right {α : Type u_1} {β : Type u_3} {γ : Type u_10} {A : Set γ} (G : Graph α β) (X : Set γ) :

G.multiApex (A \ X) = (G.multiApex A).deleteVerts (Sum.inr '' X)

source

theorem Graph.multiApex_eDegree_inr {α : Type u_1} {β : Type u_3} {γ : Type u_10} {A : Set γ} (G : Graph α β) {a : γ} (ha : a ∈ A) :

(G.multiApex A).eDegree (Sum.inr a) = G.vertexSet.encard

source

theorem Graph.multiApex_eDegree_inl {α : Type u_1} {β : Type u_3} {γ : Type u_10} {A : Set γ} (G : Graph α β) {x : α} (ha : x ∈ G.vertexSet) :

(G.multiApex A).eDegree (Sum.inl x) = G.eDegree x + A.encard

source

def Graph.apex {α : Type u_1} {β : Type u_3} (G : Graph α β) :

Graph (Option α) (β ⊕ α)

The graph with vertices V(G) ∪ {none} and edges E(G) ∪ V(G), where the new edges go to the apex vertex.

Equations

G.apex = ((Graph.map (Sum.elim some fun (x : Unit) => none) (G.multiApex Set.univ)).edgeMap (Sum.elim Sum.inl fun (x : α × Unit) => Sum.inr x.1) ⋯).copy ⋯ ⋯ ⋯

Instances For

source

@[simp]

theorem Graph.edgeSet_apex {α : Type u_1} {β : Type u_3} (G : Graph α β) :

G.apex.edgeSet = Sum.inl '' G.edgeSet ∪ Sum.inr '' G.vertexSet

source

@[simp]

theorem Graph.vertexSet_apex {α : Type u_1} {β : Type u_3} (G : Graph α β) :

G.apex.vertexSet = insert none (some '' G.vertexSet)

source

theorem Graph.apex_isLink_eq_match {α : Type u_1} {β : Type u_3} (G : Graph α β) :

G.apex.IsLink = fun (e : β ⊕ α) (x y : Option α) => match e, x, y with | Sum.inl e, some x, some y => G.IsLink e x y | Sum.inr e, some x, none => x ∈ G.vertexSet ∧ e = x | Sum.inr e, none, some x => x ∈ G.vertexSet ∧ e = x | x, x_1, x_2 => False

source

@[simp]

theorem Graph.apex_isLink_inl_iff {α : Type u_1} {β : Type u_3} {G : Graph α β} {e : β} {x y : α} :

G.apex.IsLink (Sum.inl e) (some x) (some y) ↔ G.IsLink e x y

source

@[simp]

theorem Graph.apex_isLink_inr_left_iff {α : Type u_1} {β : Type u_3} {G : Graph α β} {e x : α} :

G.apex.IsLink (Sum.inr e) (some x) none ↔ x ∈ G.vertexSet ∧ e = x

source

@[simp]

theorem Graph.apex_isLink_inr_right_iff {α : Type u_1} {β : Type u_3} {G : Graph α β} {e x : α} :

G.apex.IsLink (Sum.inr e) none (some x) ↔ x ∈ G.vertexSet ∧ e = x

source

@[simp]

theorem Graph.apex_isLoopAt_none {α : Type u_1} {β : Type u_3} {G : Graph α β} {e : β ⊕ α} :

¬G.apex.IsLoopAt e none

source

@[simp]

theorem Graph.apex_not_isLink_inl_none_left {α : Type u_1} {β : Type u_3} {G : Graph α β} {e : β} {x : Option α} :

¬G.apex.IsLink (Sum.inl e) none x

source

@[simp]

theorem Graph.apex_not_isLink_inl_none_right {α : Type u_1} {β : Type u_3} {G : Graph α β} {e : β} {x : Option α} :

¬G.apex.IsLink (Sum.inl e) x none

source

@[simp]

theorem Graph.apex_not_isLink_inr_some_some {α : Type u_1} {β : Type u_3} {G : Graph α β} {e x y : α} :

¬G.apex.IsLink (Sum.inr e) (some x) (some y)

source

theorem Graph.apex_inc_eq_match {α : Type u_1} {β : Type u_3} {G : Graph α β} :

G.apex.Inc = fun (e : β ⊕ α) (x : Option α) => match e, x with | Sum.inl e, some x => G.Inc e x | Sum.inr y, some x => x ∈ G.vertexSet ∧ x = y | Sum.inr y, none => y ∈ G.vertexSet | x, x_1 => False

source

@[simp]

theorem Graph.apex_adj_some_some_iff {α : Type u_1} {β : Type u_3} {G : Graph α β} {x y : α} :

G.apex.Adj (some x) (some y) ↔ G.Adj x y

source

@[simp]

theorem Graph.apex_adj_some_none {α : Type u_1} {β : Type u_3} {G : Graph α β} {x : α} :

G.apex.Adj (some x) none ↔ x ∈ G.vertexSet

source

@[simp]

theorem Graph.apex_adj_none_some {α : Type u_1} {β : Type u_3} {G : Graph α β} {x : α} :

G.apex.Adj none (some x) ↔ x ∈ G.vertexSet

source

@[simp]

theorem Graph.apex_isLoopAt_inl {α : Type u_1} {β : Type u_3} {G : Graph α β} {e : β} {x : α} :

G.apex.IsLoopAt (Sum.inl e) (some x) ↔ G.IsLoopAt e x

source

@[simp]

theorem Graph.apex_not_isLoopAt_inr {α : Type u_1} {β : Type u_3} (G : Graph α β) {y : Option α} {e : α} :

¬G.apex.IsLoopAt (Sum.inr e) y

source

@[simp]

theorem Graph.apex_not_isLoopAt_none {α : Type u_1} {β : Type u_3} (G : Graph α β) {e : β ⊕ α} :

¬G.apex.IsLoopAt e none

source

@[simp]

theorem Graph.apex_not_adj_none {α : Type u_1} {β : Type u_3} (G : Graph α β) :

¬G.apex.Adj none none

source

@[simp]

theorem Graph.apex_loopless_iff {α : Type u_1} {β : Type u_3} {G : Graph α β} :

G.apex.Loopless ↔ G.Loopless

source

theorem Graph.Loopless.apex_loopless {α : Type u_1} {β : Type u_3} {G : Graph α β} :

G.Loopless → G.apex.Loopless

Alias of the reverse direction of Graph.apex_loopless_iff.

source

@[simp]

theorem Graph.apex_simple_iff {α : Type u_1} {β : Type u_3} {G : Graph α β} :

G.apex.Simple ↔ G.Simple

source

theorem Graph.Simple.apex_simple {α : Type u_1} {β : Type u_3} {G : Graph α β} :

G.Simple → G.apex.Simple

Alias of the reverse direction of Graph.apex_simple_iff.

source

theorem Graph.apex_connected {α : Type u_1} {β : Type u_3} (G : Graph α β) :

G.apex.Connected

source

theorem Graph.apex_delete_none {α : Type u_1} {β : Type u_3} (G : Graph α β) :

G.apex.deleteVerts {none } = (map some G).edgeMap Sum.inl ⋯

source

theorem Graph.apex_deleteVerts {α : Type u_1} {β : Type u_3} (G : Graph α β) (X : Set α) :

(G.deleteVerts X).apex = G.apex.deleteVerts (some '' X)

source

theorem Graph.apex_eDegree {α : Type u_1} {β : Type u_3} {G : Graph α β} {v : α} (hv : v ∈ G.vertexSet) :

G.apex.eDegree (some v) = G.eDegree v + 1

source

theorem Graph.PreconnGE.apex {α : Type u_1} {β : Type u_3} {G : Graph α β} {n : ℕ} (hG : G.PreconnGE n) :

G.apex.PreconnGE (n + 1)

source

theorem Graph.ConnGE.apex {α : Type u_1} {β : Type u_3} {G : Graph α β} {n : ℕ} (hG : G.ConnGE n) (hnt : G.vertexSet.Nontrivial) :

G.apex.ConnGE (n + 1)

source

theorem Graph.IsWalk.isWalk_apex {α : Type u_1} {β : Type u_3} {G : Graph α β} {W : WList α β} (hW : G.IsWalk W) :

G.apex.IsWalk (WList.edgeMap Sum.inl (WList.map some W))

source

theorem Graph.IsPath.isPath_apex {α : Type u_1} {β : Type u_3} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) :

G.apex.IsPath (WList.edgeMap Sum.inl (WList.map some P))

source

theorem Graph.IsCyclicWalk.isCyclicWalk_apex {α : Type u_1} {β : Type u_3} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) :

G.apex.IsCyclicWalk (WList.edgeMap Sum.inl (WList.map some C))

source

theorem Graph.IsPath.isCyclicWalk_apex {α : Type u_1} {β : Type u_3} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) (hPne : P.Nonempty) :

G.apex.IsCyclicWalk ((WList.cons none (Sum.inr P.first) (WList.edgeMap Sum.inl (WList.map some P))).concat (Sum.inr P.last) none)

Any nontrivial path in G can be extended to a cycle of G.apex via the apex.

source

theorem Graph.apex_isBond_setLinkEdges_singleton {α : Type u_1} {β : Type u_3} {x : α} (G : Graph α β) (hx : x ∈ G.vertexSet) :

G.apex.IsBond E(G.apex, {some x}, G.apex.vertexSet \ {some x})