Prove2Me

Parity agreement for odd-degree vertices in a finite bipartite graph

Proved
ProofsInTheBook.Chapter39.bipartite_odd_degree_card_eq_mod_two

by xiangyazi24 · Sep 12, 2026 · Mathlib c5ea003 (Lean v4.30.0)

auxiliary-lemmabook-chapter-43combinatoricsgraph-theorylean4proofs-from-the-book

Let R,SR,S be finite sets and let E⊆R×SE\subseteq R\times S be a decidable incidence relation. Define deg⁡R(r)=∣{s∈S:(r,s)∈E}∣\deg_R(r)=|\{s\in S:(r,s)\in E\}| and deg⁡S(s)=∣{r∈R:(r,s)∈E}∣\deg_S(s)=|\{r\in R:(r,s)\in E\}|. Then

∣{r∈R:deg⁡R(r) is odd}∣≡∣{s∈S:deg⁡S(s) is odd}∣(mod2).|\{r\in R:\deg_R(r)\text{ is odd}\}|\equiv|\{s\in S:\deg_S(s)\text{ is odd}\}|\pmod 2.
Preamble
import Init
import Mathlib
import Mathlib.Data.Fin.Tuple.Sort
import Definitions.Def_P2MAssembly_Chapter39
set_option autoImplicit true
open ProofsInTheBook.Chapter39
open SignedPermutation
Formal statement
theorem ProofsInTheBook.Chapter39.bipartite_odd_degree_card_eq_mod_two
    {R S : Type*} [Fintype R] [Fintype S]
    (edge : R → S → Prop) [DecidableRel edge] :
    (Fintype.card {r : R // Odd (Fintype.card {s : S // edge r s})} : ZMod 2) =
      (Fintype.card {s : S // Odd (Fintype.card {r : R // edge r s})} : ZMod 2) := by sorry
Source
Original formalization: https://github.com/xiangyazi24/proof_in_the_book/blob/88d88d141768cded75e782c525ef1bf04b8fe220/ProofsInTheBook/Chapter39Tucker.lean#L2292. Topic: Aigner and Ziegler, Proofs from THE BOOK, 6th edition, Chapter 43, “The chromatic number of Kneser graphs”, pp. 301–305 (https://doi.org/10.1007/978-3-662-57265-8_43).

View graph