English
Under a similar finiteness assumption, IsPerfectMatching is characterized by degree 1 at every vertex.
Русский
С аналогичным ограничением на концевые множества соседей, совершенное совпадение эквивалентно степеням 1 на каждой вершине.
LaTeX
$$IsPerfectMatching(M) \iff \forall v, M.degree(v)=1$$
Lean4
theorem even_iff_exists_isMatching {u : Set V} (hc : G.IsClique u) (hu : u.Finite) :
Even u.ncard ↔ ∃ (M : Subgraph G), M.verts = u ∧ M.IsMatching :=
by
refine
⟨fun h ↦ ?_, by
rintro ⟨M, rfl, hMr⟩
simpa [Set.ncard_eq_toFinset_card _ hu, Set.toFinite_toFinset, ← Set.toFinset_card] using
@hMr.even_card _ _ _ hu.fintype⟩
obtain ⟨t, u, rfl, hd, hcard⟩ := Set.exists_union_disjoint_ncard_eq_of_even h
obtain ⟨f⟩ : Nonempty (t ≃ u) :=
by
rw [← Cardinal.eq, ← t.cast_ncard (Set.finite_union.mp hu).1, ← u.cast_ncard (Set.finite_union.mp hu).2]
exact congrArg Nat.cast hcard
exact
Subgraph.IsMatching.exists_of_disjoint_sets_of_equiv hd f fun v ↦
hc (by simp) (by simp) <| hd.ne_of_mem (by simp) (by simp)
