def MatchingPolytope.IsMatchingSet {V : Type u_1} (G : SimpleGraph V) (M : Set (Sym2 V)) : Prop

theorem MatchingPolytope.indicator_is_matching {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (x : Sym2 V → ℕ) (_hx01 : ∀ e ∈ G.edgeFinset, x e = 0 ∨ x e = 1) (hdeg : ∀ (v : V), ∑ e ∈ G.incidenceFinset v, x e ≤ 1) : IsMatchingSet G {e : Sym2 V | e ∈ G.edgeFinset ∧ x e = 1}