def IndependentTransversal.IsIndependentTransversal {V : Type u_1} {r : ℕ} (G : SimpleGraph V) (parts : Fin r → Finset V) (f : Fin r → V) : Prop

A function f : Fin r → V is an independent transversal for the partition parts : Fin r → Finset V of $V$ in the graph $G$ if it picks one vertex from each part ($f i \in $ parts i) and its image is an independent set in $G$.

theorem IndependentTransversal.IsIndependentTransversal.of_subset {V : Type u_1} {G : SimpleGraph V} {r : ℕ} {parts parts' : Fin r → Finset V} (h_sub : ∀ (i : Fin r), parts' i ⊆ parts i) {f : Fin r → V} (hf : IsIndependentTransversal G parts' f) : IsIndependentTransversal G parts f

An independent transversal for smaller parts parts' is also one for any enlargement parts ⊇ parts'.

theorem IndependentTransversal.lll_independent_transversal_equal_parts {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (r : ℕ) (parts : Fin r → Finset V) (k : ℕ) (hk : 0 < k) (h_card : ∀ (i : Fin r), (parts i).card = k) (h_disjoint : ∀ (i j : Fin r), i ≠ j → Disjoint (parts i) (parts j)) (h_lll : 2 * Real.exp 1 * ↑G.maxDegree ≤ ↑k) : ∃ (f : Fin r → V), IsIndependentTransversal G parts f

LLL-based existence of an independent transversal in the equal-part case: if every part has the same size $k$ and $2 e \Delta(G) \le k$, then there is an independent transversal, obtained by sampling each $f(i)$ uniformly from parts i and applying the LLL.

theorem IndependentTransversal.independent_transversal_exists {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (r : ℕ) (parts : Fin r → Finset V) (h_nonempty : ∀ (i : Fin r), (parts i).Nonempty) (h_disjoint : ∀ (i j : Fin r), i ≠ j → Disjoint (parts i) (parts j)) (h_size : ∀ (i : Fin r), 2 * Real.exp 1 * ↑G.maxDegree ≤ ↑(parts i).card) : ∃ (f : Fin r → V), IsIndependentTransversal G parts f

Theorem 6.3.1 (Independent Transversal): if $V$ is partitioned into disjoint parts each of size at least $2 e \Delta(G)$, then there is an independent transversal selecting one vertex per part with pairwise non-adjacent images. Proven by trimming each part to size exactly $\lceil 2 e \Delta \rceil$ and invoking the equal-parts LLL version.