Intersection and union of graphs

This file defines the lattice-like structures on graphs.

Main results

• SemilatticeInf (Graph α β)

Implementation notes

Intersections are defined here as the maximal mutual subgraph of the given graphs. This has the effect of, when taking the intersection of non-compatible graphs, any non-compatible edges are removed.

TODO

• Add ConditionallyCompleteCompleteLatticeInf (Graph α β) after splitting ConditionallyCompleteCompleteLattice.

@[instance_reducible]

instance Graph.instSemilatticeInf {α : Type u_1} {β : Type u_2} : SemilatticeInf (Graph α β)

The infimum of two graphs G and H. The edges are precisely those on which G and H agree, and the edge set is a subset of E(G) ∩ E(H), with equality if G and H are compatible.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Graph.vertexSet_inf {α : Type u_1} {β : Type u_2} (G H : Graph α β) : (G ⊓ H).vertexSet = G.vertexSet ∩ H.vertexSet

theorem Graph.edgeSet_inf {α : Type u_1} {β : Type u_2} (G H : Graph α β) : (G ⊓ H).edgeSet = {e : β | e ∈ G.edgeSet ∩ H.edgeSet ∧ ∀ (x y : α), G.IsLink e x y ↔ H.IsLink e x y}

@[simp]

theorem Graph.inf_isLink {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β} : (G ⊓ H).IsLink e x y ↔ G.IsLink e x y ∧ H.IsLink e x y

@[simp]

theorem Graph.inf_inc_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} : (G ⊓ H).Inc e x ↔ ∃ (y : α), G.IsLink e x y ∧ H.IsLink e x y

@[simp]

theorem Graph.inf_isLoopAt_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} : (G ⊓ H).IsLoopAt e x ↔ G.IsLoopAt e x ∧ H.IsLoopAt e x

@[simp]

theorem Graph.inf_isNonloopAt_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} : (G ⊓ H).IsNonloopAt e x ↔ ∃ (y : α), y ≠ x ∧ G.IsLink e x y ∧ H.IsLink e x y

@[simp]

theorem Graph.disjoint_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} : Disjoint G H ↔ Disjoint G.vertexSet H.vertexSet

theorem Graph.Compatible.edgeSet_inf {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.Compatible H) : (G ⊓ H).edgeSet = G.edgeSet ∩ H.edgeSet