def BipartiteDoubleCover.IsIndepFinset {W : Type u_2} [DecidableEq W] (G : SimpleGraph W) [DecidableRel G.Adj] (S : Finset W) : Prop

A finset $S$ of vertices of $G$ is independent if no two distinct vertices in $S$ are adjacent.

@[implicit_reducible]

instance BipartiteDoubleCover.instDecIsIndepFinset {W : Type u_2} [DecidableEq W] (G : SimpleGraph W) [DecidableRel G.Adj] : DecidablePred (IsIndepFinset G)

Decidability of the independence predicate on finsets when adjacency in $G$ is decidable.

def BipartiteDoubleCover.indepSets {W : Type u_2} [Fintype W] [DecidableEq W] (G : SimpleGraph W) [DecidableRel G.Adj] : Finset (Finset W)

The finset of all independent vertex sets of $G$.

def BipartiteDoubleCover.numIndepSets {W : Type u_2} [Fintype W] [DecidableEq W] (G : SimpleGraph W) [DecidableRel G.Adj] : ℕ

The number of independent vertex sets of $G$, denoted $i(G)$.

theorem BipartiteDoubleCover.swapping_trick_injection {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ∃ (f : Finset V × Finset V → Finset (V ⊕ V)), (∀ p ∈ indepSets G ×ˢ indepSets G, f p ∈ indepSets G.bipartiteDoubleCover) ∧ ∀ p₁ ∈ indepSets G ×ˢ indepSets G, ∀ p₂ ∈ indepSets G ×ˢ indepSets G, f p₁ = f p₂ → p₁ = p₂

Swapping-trick injection from pairs of independent sets of $G$ into independent sets of the bipartite double cover $G \times K_2$, establishing the inequality $i(G)^2 \le i(G \times K_2)$.

theorem BipartiteDoubleCover.indep_sets_sq_le_bipartite_double_cover {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : numIndepSets G ^ 2 ≤ numIndepSets G.bipartiteDoubleCover

Lemma 10.4.13 (Zhao): the square of the number of independent sets of $G$ is at most the number of independent sets of its bipartite double cover, $i(G)^2 \le i(G \times K_2)$.