Documentation

TauCeti.Combinatorics.Graph.Union

Unions of compatible multigraphs #

This file constructs the union of two compatible Graphs. Its vertices and edges are the set-theoretic unions, and an edge is linked exactly when it is linked in either input graph. Compatibility is essential: a shared edge must not acquire two different pairs of endpoints. The incident-edge, loop, and nonloop incident-edge sets at a vertex are likewise unions of the corresponding sets in the two inputs, without any finiteness assumptions.

The union is the least common supergraph of its inputs. Compatible unions commute, and unions of three pairwise compatible graphs associate. These facts let graph constructions grow a subgraph one compatible piece at a time while retaining the original vertex and edge types.

The interface is the compatible fragment of the union design in Mathlib pull request #38337. Unlike that proposal, no choice of incidence is made for incompatible shared edges.

source
def Graph.Compatible.union {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.Compatible H) :
Graph α β

The union of compatible graphs. Its vertices, edges, and links are the corresponding unions.

Instances For
    source
    @[simp]
    theorem Graph.Compatible.vertexSet_union {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.Compatible H) :
    h.union.vertexSet = G.vertexSet ∪ H.vertexSet
    source
    @[simp]
    theorem Graph.Compatible.edgeSet_union {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.Compatible H) :
    h.union.edgeSet = G.edgeSet ∪ H.edgeSet
    source
    @[simp]
    theorem Graph.Compatible.union_inc_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} {e : β} {x : α} (h : G.Compatible H) :
    h.union.Inc e x ↔ G.Inc e x ∨ H.Inc e x
    source
    @[simp]
    theorem Graph.Compatible.union_adj_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} {x y : α} (h : G.Compatible H) :
    h.union.Adj x y ↔ G.Adj x y ∨ H.Adj x y
    source
    @[simp]
    theorem Graph.Compatible.union_isLoopAt_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} {e : β} {x : α} (h : G.Compatible H) :
    h.union.IsLoopAt e x ↔ G.IsLoopAt e x ∨ H.IsLoopAt e x
    source
    @[simp]
    theorem Graph.Compatible.union_isNonloopAt_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} {e : β} {x : α} (h : G.Compatible H) :
    h.union.IsNonloopAt e x ↔ G.IsNonloopAt e x ∨ H.IsNonloopAt e x
    source
    @[simp]
    theorem Graph.Compatible.incidenceSet_union {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.Compatible H) (x : α) :
    incidenceSet x = incidenceSet x ∪ incidenceSet x

    Incident edge identities in a compatible union are those incident in either input.

    source
    @[simp]
    theorem Graph.Compatible.loopSet_union {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.Compatible H) (x : α) :
    loopSet x = loopSet x ∪ loopSet x

    Loop identities in a compatible union are those that are loops in either input.

    source
    theorem Graph.Compatible.incidenceSet_sdiff_loopSet_union {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.Compatible H) (x : α) :
    incidenceSet x \ loopSet x = incidenceSet x \ loopSet x ∪ incidenceSet x \ loopSet x

    Compatibility ensures that a shared edge cannot be a loop in just one input. Consequently, nonloop incident edges also commute with union.

    source
    @[simp]
    theorem Graph.Compatible.left_le_union {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.Compatible H) :
    G ≤ h.union

    The left input is a subgraph of a compatible union.

    source
    @[simp]
    theorem Graph.Compatible.right_le_union {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.Compatible H) :
    H ≤ h.union

    The right input is a subgraph of a compatible union.

    source
    @[simp]
    theorem Graph.Compatible.union_le_iff {α : Type u_1} {β : Type u_2} {G H K : Graph α β} (h : G.Compatible H) :
    h.union ≤ K ↔ G ≤ K ∧ H ≤ K

    A compatible union is contained in a graph exactly when both inputs are contained in it.

    source
    theorem Graph.Compatible.union_comm {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.Compatible H) :
    h.union = ⋯.union

    Compatible union is commutative.

    source
    theorem Graph.Compatible.union_compatible {α : Type u_1} {β : Type u_2} {G H K : Graph α β} (hGH : G.Compatible H) (hGK : G.Compatible K) (hHK : H.Compatible K) :
    hGH.union.Compatible K

    The union of G and H is compatible with K when all three graphs are pairwise compatible.

    source
    theorem Graph.Compatible.compatible_union {α : Type u_1} {β : Type u_2} {G H K : Graph α β} (hGH : G.Compatible H) (hGK : G.Compatible K) (hHK : H.Compatible K) :
    G.Compatible hHK.union

    G is compatible with the union of H and K when all three graphs are pairwise compatible.

    source
    theorem Graph.Compatible.union_assoc {α : Type u_1} {β : Type u_2} {G H K : Graph α β} (hGH : G.Compatible H) (hGK : G.Compatible K) (hHK : H.Compatible K) :
    ⋯.union = ⋯.union

    Compatible union is associative for three pairwise compatible graphs.

    source
    theorem Graph.IsSubgraph.union_le {α : Type u_1} {β : Type u_2} {G H K : Graph α β} (hG : G ≤ K) (hH : H ≤ K) :
    ⋯.union ≤ K

    The compatible union of two subgraphs of K remains a subgraph of K.