card_odd_degree — Mathlib

English

The same 0 or 2 dichotomy for the number of odd-degree vertices, stated via Finset/Cardinalities.

Русский

Та же зависимость: число вершин нечетной степени равно 0 или 2.

LaTeX

$$$ \text{Fintype.card} \{v : V | \text{Odd} (G.degree v)\} = 0 \;\vee\; \text{Fintype.card} \{v : V | \text{Odd} (G.degree v)\} = 2 $$$

Lean4

theorem card_odd_degree [Fintype V] [DecidableRel G.Adj] {u v : V} {p : G.Walk u v} (ht : p.IsEulerian) :
    Fintype.card {v : V | Odd (G.degree v)} = 0 ∨ Fintype.card {v : V | Odd (G.degree v)} = 2 :=
  by
  rw [← Set.toFinset_card]
  apply IsEulerian.card_filter_odd_degree ht
  ext v
  simp

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