English
If a subset s is disjoint from universal vertices and is not larger than the universal set, one can extend s within universal vertices to obtain a matching.
Русский
Если подмножество не пересекается с универсальными вершинами и не больше по кардиналу самого множества универсальных вершин, то можно дополнить s внутри универсальных вершин так, чтобы получить несовпадение.
LaTeX
$$Exists t ⊆ G.universalVerts, ∃ M ⊆ G, M.IsMatching with verts = s ∪ t$$
Lean4
theorem exists_of_universalVerts [Finite V] {s : Set V} (h : Disjoint G.universalVerts s)
(hc : s.ncard ≤ G.universalVerts.ncard) :
∃ t ⊆ G.universalVerts, ∃ (M : Subgraph G), M.verts = s ∪ t ∧ M.IsMatching :=
by
obtain ⟨t, ht⟩ := Set.exists_subset_card_eq hc
refine ⟨t, ht.1, ?_⟩
obtain ⟨f⟩ : Nonempty (s ≃ t) := by rw [← Cardinal.eq, ← t.cast_ncard t.toFinite, ← s.cast_ncard s.toFinite, ht.2]
letI hd := Set.disjoint_of_subset_left ht.1 h
have hadj (v : s) : G.Adj v (f v) := ht.1 (f v).2 (hd.ne_of_mem (f v).2 v.2)
exact Subgraph.IsMatching.exists_of_disjoint_sets_of_equiv hd.symm f hadj
