induce_connectedComponent — Mathlib

English

If M is a matching, then the induced subgraph on M.verts ∩ c.supp is also a matching for any connected component c.

Русский

Если M — совпадение, то индуцированный подграф на M.verts ∩ c.supp также является совпадением для любой связной компоненты c.

LaTeX

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

Lean4

theorem induce_connectedComponent (h : M.IsMatching) (c : ConnectedComponent G) :
    (M.induce (M.verts ∩ c.supp)).IsMatching := by
  intro _ hv
  obtain ⟨hv, rfl⟩ := hv
  obtain ⟨w, hvw, hw⟩ := h hv
  use w
  simpa [hv, hvw, M.edge_vert hvw.symm, (M.adj_sub hvw).symm.reachable] using fun _ _ _ ↦ hw _

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