theorem BipartiteSubgraph.bne_symm {V : Type u_2} (f : V → Bool) (a b : V) : (f a != f b) = (f b != f a)

Boolean inequality != is symmetric: $(f(a) \neq f(b)) = (f(b) \neq f(a))$.

def BipartiteSubgraph.boolCut {V : Type u_1} (f : V → Bool) : Sym2 V → Bool

For a Boolean labelling f : V → Bool, boolCut f e returns true when the unordered pair e = s(u, v) is a cut edge, i.e. f u ≠ f v.

@[simp]

theorem BipartiteSubgraph.boolCut_mk {V : Type u_1} (f : V → Bool) (u v : V) : boolCut f s(u, v) = (f u != f v)

Evaluation of boolCut on an explicit pair s(u, v).

def BipartiteSubgraph.flipAt {V : Type u_2} [DecidableEq V] (v : V) (f : V → Bool) : V → Bool

flipAt v f is the Boolean labelling obtained from f by negating its value at v.

theorem BipartiteSubgraph.flipAt_involutive {V : Type u_2} [DecidableEq V] (v : V) : Function.Involutive (flipAt v)

Flipping the value at v twice returns the original labelling.

theorem BipartiteSubgraph.flipAt_bne_eq_not {V : Type u_2} [DecidableEq V] {u v : V} (huv : u ≠ v) (f : V → Bool) : (flipAt v f u != flipAt v f v) = !f u != f v

If u ≠ v, then flipping f at v toggles whether the edge {u, v} is a cut edge.

theorem BipartiteSubgraph.two_mul_card_filter_bne {V : Type u_1} [Fintype V] [DecidableEq V] (u v : V) (huv : u ≠ v) : 2 * {f : V → Bool | (f u != f v) = true}.card = Fintype.card (V → Bool)

Exactly half of the Boolean labellings f : V → Bool separate the pair {u, v} when u ≠ v; equivalently, twice that count equals the total number of labellings.

theorem BipartiteSubgraph.double_count_sum {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : 2 * ∑ f : V → Bool, {e ∈ G.edgeFinset | boolCut f e = true}.card = G.edgeFinset.card * Fintype.card (V → Bool)

Double-counting identity: summing the number of cut edges over all Boolean labellings equals half of |E(G)| · 2^{|V|}.

theorem BipartiteSubgraph.exists_bipartite_subgraph_half_edges {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ∃ (f : V → Bool), G.edgeFinset.card / 2 ≤ {e ∈ G.edgeFinset | boolCut f e = true}.card

(Theorem 1.0.1, first form) There exists a Boolean labelling $f : V \to \{0,1\}$ whose cut contains at least $\lfloor |E(G)|/2 \rfloor$ edges.

def BipartiteSubgraph.cutGraph {V : Type u_2} (G : SimpleGraph V) (f : V → Bool) : SimpleGraph V

The cut subgraph of G induced by a Boolean labelling f: the subgraph consisting of edges {u, v} of G with f u ≠ f v.

theorem BipartiteSubgraph.cutGraph_le {V : Type u_1} (G : SimpleGraph V) (f : V → Bool) : cutGraph G f ≤ G

The cut subgraph cutGraph G f is a subgraph of G.

theorem BipartiteSubgraph.cutGraph_isBipartite {V : Type u_1} (G : SimpleGraph V) (f : V → Bool) : (cutGraph G f).Colorable 2

The cut subgraph cutGraph G f is bipartite (2-colorable), using f as the coloring.

theorem BipartiteSubgraph.cutGraph_edgeFinset_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (f : V → Bool) [Fintype ↑(cutGraph G f).edgeSet] : (cutGraph G f).edgeFinset = {e ∈ G.edgeFinset | boolCut f e = true}

The edge set of cutGraph G f is precisely the set of cut edges of G under f.

theorem BipartiteSubgraph.exists_bipartite_subgraph {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ∃ H ≤ G, H.Colorable 2 ∧ ∀ [inst : Fintype ↑H.edgeSet], G.edgeFinset.card / 2 ≤ H.edgeFinset.card

(Theorem 1.0.1) Every graph $G$ with $m$ edges has a bipartite subgraph $H \le G$ with at least $\lfloor m/2 \rfloor$ edges.