Odd independent sets

DefinitionOdd independent set#✓fully proved

A set \(S\) of vertices of a simple graph \(G\) is odd independent if \(S\) is an independent set of \(G\) and, for every vertex \(v \notin S\), the set of neighbours of \(v\) that lie in \(S\) is finite and is either empty or has an odd number of elements.

def IsOddIndependent (G : SimpleGraph V) (S : Set V) : Prop :=
  G.IsIndepSet S ∧
    ∀ v : V, v ∉ S →
      (G.neighborSet v ∩ S).Finite ∧
        ((G.neighborSet v ∩ S) = ∅ ∨ Odd (G.neighborSet v ∩ S).ncard)

Used by 5

Used byOutside vertices see an empty or odd part of an odd independent set · Outside vertices have finitely many neighbours in an odd independent set · Odd independent sets are independent · The empty set is odd independent · Singletons are odd independent

TheoremOdd independent sets are independent#✓fully proved

If \(S\) is an odd independent set of a simple graph \(G\), then \(S\) is an independent set of \(G\): no two distinct vertices of \(S\) are adjacent.

theorem IsOddIndependent.isIndepSet {G : SimpleGraph V} {S : Set V}
    (h : G.IsOddIndependent S) : G.IsIndepSet S

Uses 1

Statement usesOdd independent set

TheoremOutside vertices have finitely many neighbours in an odd independent set#✓fully proved

Let \(S\) be an odd independent set of a simple graph \(G\) and let \(v\) be a vertex with \(v \notin S\). Then only finitely many neighbours of \(v\) lie in \(S\).

theorem IsOddIndependent.finite_inter {G : SimpleGraph V} {S : Set V}
    (h : G.IsOddIndependent S) (v : V) (hv : v ∉ S) :
    (G.neighborSet v ∩ S).Finite

Uses 1

Statement usesOdd independent set

TheoremOutside vertices see an empty or odd part of an odd independent set#✓fully proved

Let \(S\) be an odd independent set of a simple graph \(G\) and let \(v\) be a vertex with \(v \notin S\). Then the set of neighbours of \(v\) that lie in \(S\) is either empty or has an odd number of elements.

theorem IsOddIndependent.empty_or_odd {G : SimpleGraph V} {S : Set V}
    (h : G.IsOddIndependent S) (v : V) (hv : v ∉ S) :
    (G.neighborSet v ∩ S) = ∅ ∨ Odd (G.neighborSet v ∩ S).ncard

Uses 1

Statement usesOdd independent set

TheoremThe empty set is odd independent#✓fully proved

The empty set is odd independent in any simple graph.

theorem isOddIndependent_empty {G : SimpleGraph V} :
    G.IsOddIndependent ∅

Uses 1

Statement usesOdd independent set

TheoremSingletons are odd independent#✓fully proved

For every vertex \(a\) of a simple graph \(G\), the singleton \(\{a\}\) is odd independent in \(G\).

theorem isOddIndependent_singleton {G : SimpleGraph V} (a : V) :
    G.IsOddIndependent {a}

Uses 1

Statement usesOdd independent set

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.