English
For a Eulerian walk p from u to v in G, for any vertex x the parity of the number of edges of p incident to x is determined by whether u and v are distinct; in particular, if u ≠ v, then x ≠ u and x ≠ v implies an even count, while x = u or x = v yields an odd count.
Русский
Для эйлерова следа p от u до v в графе G, для любой вершины x парность количества ребер трека, инцидентных x, определяется тем, различны ли концы следа; если u ≠ v, то вершины x, не равные u и v, имеют чётное число инцидентных ребер, а для x = u или x = v число нечетное.
LaTeX
$$$ \text{Even} \big(p.edges.countP (\lambda e\, x \in e)\big) \iff u \neq v \rightarrow x \neq u \land x \neq v $$$
Lean4
theorem even_countP_edges_iff {u v : V} {p : G.Walk u v} (ht : p.IsTrail) (x : V) :
Even (p.edges.countP fun e => x ∈ e) ↔ u ≠ v → x ≠ u ∧ x ≠ v := by
induction p with
| nil => simp
| cons huv p ih =>
rw [cons_isTrail_iff] at ht
specialize ih ht.1
simp only [List.countP_cons, Ne, edges_cons, Sym2.mem_iff]
split_ifs with h
· rw [decide_eq_true_eq] at h
obtain (rfl | rfl) := h
· rw [Nat.even_add_one, ih]
simp only [huv.ne, imp_false, Ne, not_false_iff, true_and, not_forall, Classical.not_not, exists_prop, not_true,
false_and, and_iff_right_iff_imp]
rintro rfl rfl
exact G.loopless _ huv
· rw [Nat.even_add_one, ih, ← not_iff_not]
simp only [huv.ne.symm, Ne, not_true, false_and, not_forall, not_false_iff, exists_prop, and_true,
Classical.not_not, true_and, iff_and_self]
rintro rfl
exact huv.ne
· grind
