isPerfectMatching_iff — Mathlib

English

A subgraph M is a perfect matching if and only if every vertex has exactly one neighbor in M.

Русский

Подграф M — совершенное совпадение тогда и только тогда, когда каждая вершина имеет ровно одного соседа в M.

LaTeX

$$IsPerfectMatching(M) \iff (forall v, exists! w, M.Adj(v,w))$$

Lean4

theorem isPerfectMatching_iff : M.IsPerfectMatching ↔ ∀ v, ∃! w, M.Adj v w :=
  by
  refine ⟨?_, fun hm => ⟨fun v _ => hm v, fun v => ?_⟩⟩
  · rintro ⟨hm, hs⟩ v
    exact hm (hs v)
  · obtain ⟨w, hw, -⟩ := hm v
    exact M.edge_vert hw

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