Notation: Binary Vectors

Statement

Throughout this work we use binary vectors over ℤ₂ (equivalently 𝔽₂) to indicate collections of vertices, edges, and cycles of a graph G. We identify the binary vector associated to a set of vertices, edges, or cycles with the set itself. Addition of binary vectors corresponds to symmetric difference of sets.

Main Results

• charVec: characteristic vector of a set S over a type α as a function α → ZMod 2
• charVec_mem: charVec S v = 1 ↔ v ∈ S
• charVec_symmDiff: χ(S △ T) = χ(S) + χ(T), the key provable content

Corollaries

• charVec_symmDiff_self: χ(S △ S) = 0
• charVec_injective: charVec is injective (distinct sets have distinct vectors)

Definition of characteristic vector

noncomputable def charVec {α : Type u_1} (S : Set α) : α → ZMod 2

The characteristic vector of a set S over a type α, taking values in ZMod 2. charVec S v = 1 if v ∈ S and charVec S v = 0 otherwise.

Equations

• charVec S = S.indicator 1

Basic properties

theorem charVec_apply_of_mem {α : Type u_1} {S : Set α} {v : α} (hv : v ∈ S) : charVec S v = 1

theorem charVec_apply_of_not_mem {α : Type u_1} {S : Set α} {v : α} (hv : v ∉ S) : charVec S v = 0

@[simp]

theorem charVec_mem {α : Type u_1} {S : Set α} {v : α} : charVec S v = 1 ↔ v ∈ S

@[simp]

theorem charVec_not_mem {α : Type u_1} {S : Set α} {v : α} : charVec S v = 0 ↔ v ∉ S

@[simp]

theorem charVec_empty {α : Type u_1} : charVec ∅ = 0

@[simp]

theorem charVec_univ {α : Type u_1} : charVec Set.univ = 1

Main theorem: symmetric difference corresponds to addition

theorem charVec_symmDiff {α : Type u_1} (S T : Set α) : charVec (symmDiff S T) = charVec S + charVec T

The key provable content: the characteristic vector of the symmetric difference of two sets equals the sum of their characteristic vectors in ZMod 2. This formalizes the identification of binary vector addition with symmetric difference of sets.

Corollaries and immediate consequences

@[simp]

theorem charVec_symmDiff_self {α : Type u_1} (S : Set α) : charVec (symmDiff S S) = 0

theorem charVec_ext_iff {α : Type u_1} (S T : Set α) : charVec S = charVec T ↔ S = T

theorem charVec_injective {α : Type u_1} : Function.Injective charVec

charVec is injective: distinct sets have distinct characteristic vectors.

theorem charVec_subset_iff {α : Type u_1} (S T : Set α) : (∀ (v : α), charVec S v = 1 → charVec T v = 1) ↔ S ⊆ T

@[simp]

theorem charVec_compl_add {α : Type u_1} (S : Set α) (v : α) : charVec Sᶜ v + charVec S v = 1

theorem charVec_union {α : Type u_1} (S T : Set α) : charVec (S ∪ T) = charVec S + charVec T + charVec (S ∩ T)

SimpleGraph notation

@[reducible, inline]

abbrev vertexSetOf (V : Type u_2) : Set V

For a simple graph G on vertex type V, the vertex set is Set.univ : Set V.

Equations

• vertexSetOf V = Set.univ

@[reducible, inline]

abbrev edgeSetOf (E : Type u_2) : Set E

For a simple graph G on vertex type V with edge type E, the edge set is Set.univ : Set E.

Equations

• edgeSetOf E = Set.univ