isPerfectMatching_iff_forall_degree

English

With finite neighbor sets, M is a perfect matching iff every vertex has degree 1 inside M whenever v is in M.verts.

Русский

При конечных множествах соседей M является совершенным совпадением тогда и только тогда, когда для каждой вершины, принадлежащей M.verts, степень внутри M равна 1.

LaTeX

$$Forall v, Fintype (M.neighborSet v) → (IsPerfectMatching(M) \iff ∀ v, v∈M.verts → M.degree(v)=1)$$

Lean4

theorem isPerfectMatching_iff_forall_degree [∀ v, Fintype (M.neighborSet v)] :
    M.IsPerfectMatching ↔ ∀ v, M.degree v = 1 := by simp [degree_eq_one_iff_unique_adj, isPerfectMatching_iff]

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