even_length_iff_congr — Mathlib

English

For any coloring c of G by Bool and any walk p from u to v, the length parity of p equals whether c(u) equals c(v).

Русский

Для любой раскраски c графа G битовыми цветами и любого пешехода p от u до v, четность длины p равна тому, равны ли цвета концов: c(u) = c(v).

LaTeX

$$Even p.length ↔ (c u ↔ c v)$$

Lean4

theorem even_length_iff_congr {α} {G : SimpleGraph α} (c : G.Coloring Bool) {u v : α} (p : G.Walk u v) :
    Even p.length ↔ (c u ↔ c v) := by
  induction p with
  | nil => simp
  | @cons u v w h p ih =>
    simp only [Walk.length_cons, Nat.even_add_one]
    have : ¬c u = true ↔ c v = true := by
      rw [← not_iff, ← Bool.eq_iff_iff]
      exact c.valid h
    tauto

Похожие утверждения