English
For an Eulerian walk p from u to v in G, the parity of G.degree(x) is even exactly when either u = v or x is different from both u and v; more precisely, if p is Eulerian, then for all x, Even(G.degree x) iff (u ≠ v → x ≠ u ∧ x ≠ v).
Русский
Для пути p от u до v в G чётность deg(x) равна чётной тогда, когда либо u = v, либо x не равно ни одному из концов; формально: чётность deg(x) равна чётной, если p эйлеров, тогда для всех x: Even(G.degree x) ⇔ (u ≠ v → x ≠ u ∧ x ≠ v).
LaTeX
$$$ \text{Even} (G.\text{degree } x) \iff u \neq v \rightarrow x \neq u \land x \neq v $ (при условии, что p.IsEulerian)$$
Lean4
theorem even_degree_iff {x u v : V} {p : G.Walk u v} (ht : p.IsEulerian) [Fintype V] [DecidableRel G.Adj] :
Even (G.degree x) ↔ u ≠ v → x ≠ u ∧ x ≠ v :=
by
convert ht.isTrail.even_countP_edges_iff x
rw [← Multiset.coe_countP, Multiset.countP_eq_card_filter, ← card_incidenceFinset_eq_degree]
change Multiset.card _ = _
congr 1
convert_to _ = (ht.isTrail.edgesFinset.filter (x ∈ ·)).val
rw [ht.edgesFinset_eq, G.incidenceFinset_eq_filter x]
