odd_length_iff_not_congr — Mathlib

English

For any coloring c of G by Bool and any walk p from u to v, the odd length of p is equivalent to not congruent across the endpoints.

Русский

Для любой раскраски c графа G битами и любого пути p от u до v нечетная длина соответствует несовпадению цветов концов.

LaTeX

$$Odd p.length ↔ (¬ c u ↔ c v)$$

Lean4

theorem odd_length_iff_not_congr {α} {G : SimpleGraph α} (c : G.Coloring Bool) {u v : α} (p : G.Walk u v) :
    Odd p.length ↔ (¬c u ↔ c v) :=
  by
  rw [← Nat.not_even_iff_odd, c.even_length_iff_congr p]
  tauto

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