Symmetric difference of simple graphs

Simple graphs on V form a Boolean algebra, so two graphs have a symmetric difference. Its edges are the edges of exactly one of the two graphs.

Main results

• SimpleGraph.symmDiff_adj: adjacency in the symmetric difference of two graphs.
• SimpleGraph.edgeSet_symmDiff: the edge set of a symmetric difference is the symmetric difference of the edge sets.

@[simp]

theorem SimpleGraph.symmDiff_adj {V : Type u_1} (G H : SimpleGraph V) (a b : V) : (symmDiff G H).Adj a b ↔ G.Adj a b ∧ ¬H.Adj a b ∨ H.Adj a b ∧ ¬G.Adj a b

Two vertices are adjacent in symmDiff G H exactly when they are adjacent in one of G and H but not in the other.

@[simp]

theorem SimpleGraph.edgeSet_symmDiff {V : Type u_1} (G H : SimpleGraph V) : (symmDiff G H).edgeSet = symmDiff G.edgeSet H.edgeSet

The edge set of the symmetric difference of two graphs is the symmetric difference of their edge sets.