induce_connectedComponent_isMatching

English

If M is a perfect matching, then the induced subgraph on the connected component’s supp is itself a matching.

Русский

Если M — совершенное совпадение, то индуцированный по компоненте супплемент является собой совпадением.

LaTeX

$$(M.induce c.supp).IsMatching$$

Lean4

theorem induce_connectedComponent_isMatching (h : M.IsPerfectMatching) (c : ConnectedComponent G) :
    (M.induce c.supp).IsMatching := by simpa [h.2.verts_eq_univ] using h.1.induce_connectedComponent c

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