English
In a finite graph with a perfect matching, for odd components of deleteVerts ⊤ u there is a unique bridging edge from u into that component.
Русский
В конечном графе с совершенным совпадением для нечетных компонент после удаления набора вершин существует уникальное ребро связи между u и этой компонентой.
LaTeX
$$∃! w∈u, ∃ v∈c.supp, M.Adj(v,w) ∧ v∈c.supp$$
Lean4
theorem odd_matches_node_outside [Finite V] {u : Set V} (hM : M.IsPerfectMatching)
(c : (Subgraph.deleteVerts ⊤ u).coe.oddComponents) :
∃ᵉ (w ∈ u) (v : ((⊤ : G.Subgraph).deleteVerts u).verts), M.Adj v w ∧ v ∈ c.val.supp :=
by
by_contra! h
have hMmatch : (M.induce c.val.supp).IsMatching := by
intro v hv
obtain ⟨w, hw⟩ := hM.1 (hM.2 v)
obtain ⟨⟨v', hv'⟩, ⟨hv, rfl⟩⟩ := hv
use w
have hwnu : w ∉ u := fun hw' ↦ h w hw' ⟨v', hv'⟩ (hw.1) hv
refine ⟨⟨⟨⟨v', hv'⟩, hv, rfl⟩, ?_, hw.1⟩, fun _ hy ↦ hw.2 _ hy.2.2⟩
apply ConnectedComponent.mem_coe_supp_of_adj ⟨⟨v', hv'⟩, ⟨hv, rfl⟩⟩ ⟨by trivial, hwnu⟩
simp only [Subgraph.induce_verts, Subgraph.verts_top, Set.mem_diff, Set.mem_univ, true_and, Subgraph.induce_adj,
hwnu, not_false_eq_true, and_self, Subgraph.top_adj, M.adj_sub hw.1, and_true] at hv' ⊢
trivial
apply Nat.not_even_iff_odd.2 c.prop
haveI : Fintype ↑(Subgraph.induce M (Subtype.val '' supp c.val)).verts := Fintype.ofFinite _
classical
haveI : Fintype (c.val.supp) := Fintype.ofFinite _
simpa [Subgraph.induce_verts, Subgraph.verts_top, Nat.card_eq_fintype_card, Set.toFinset_card,
Finset.card_image_of_injective, ← Nat.card_coe_set_eq] using hMmatch.even_card
