even_card — Mathlib

English

If M is a matching with finite vertex set, then the number of vertices touched by M is even.

Русский

Если M является паросочетанием с конечным числом вершин, то число вершин, затронутых M, чётно.

LaTeX

$$Even(\# M.verts)$$

Lean4

theorem even_card [Fintype M.verts] (h : M.IsMatching) : Even M.verts.toFinset.card := by
  classical
  rw [isMatching_iff_forall_degree] at h
  use M.coe.edgeFinset.card
  rw [← two_mul, ← M.coe.sum_degrees_eq_twice_card_edges]
  simp [h, Finset.card_univ]

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