theorem SimpleGraph.edmonds_polytope_perturbation {V : Type u_2} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (x : ↑G.edgeSet → ℝ) (hnn : ∀ (e : ↑G.edgeSet), 0 ≤ x e) (hdeg : ∀ (v : V), ∑ e ∈ G.incidentEdgeFinset v, x e = 1) (hodd : ∀ (S : Finset V), Odd S.card → ∑ e ∈ G.edgeCutFinset S, x e ≥ 1) (e₀ : ↑G.edgeSet) (he₀ : x e₀ ≠ 0 ∧ x e₀ ≠ 1) : ∃ (y : ↑G.edgeSet → ℝ) (z : ↑G.edgeSet → ℝ) (t : ℝ), 0 < t ∧ t < 1 ∧ y ∈ G.edmondsPolytope ∧ z ∈ G.edmondsPolytope ∧ (∀ (e : ↑G.edgeSet), x e = t * y e + (1 - t) * z e) ∧ {e : ↑G.edgeSet | y e ≠ 0 ∧ y e ≠ 1}.card < {e : ↑G.edgeSet | x e ≠ 0 ∧ x e ≠ 1}.card ∧ {e : ↑G.edgeSet | z e ≠ 0 ∧ z e ≠ 1}.card < {e : ↑G.edgeSet | x e ≠ 0 ∧ x e ≠ 1}.card

theorem SimpleGraph.edmondsPolytope_pm_decomposition_aux {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (n : ℕ) (x : ↑G.edgeSet → ℝ) (hx : x ∈ G.edmondsPolytope) (hn : {e : ↑G.edgeSet | x e ≠ 0 ∧ x e ≠ 1}.card = n) : ∃ (k : ℕ) (M : Fin k → G.Subgraph) (_ : ∀ (i : Fin k), (M i).IsPerfectMatching) (w : Fin k → ℝ), (∀ (i : Fin k), 0 ≤ w i) ∧ ∑ i : Fin k, w i = 1 ∧ ∀ (e : ↑G.edgeSet), x e = ∑ i : Fin k, w i * if ↑e ∈ (M i).edgeSet then 1 else 0