def SimpleGraph.incidentEdgeFinset {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) : Finset ↑G.edgeSet

def SimpleGraph.edgeCutFinset {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : Finset ↑G.edgeSet

def SimpleGraph.perfectMatchingIndicators {V : Type u_1} (G : SimpleGraph V) : Set (↑G.edgeSet → ℝ)

def SimpleGraph.perfectMatchingPolytope {V : Type u_1} (G : SimpleGraph V) : Set (↑G.edgeSet → ℝ)

def SimpleGraph.edmondsPolytope {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Set (↑G.edgeSet → ℝ)

theorem SimpleGraph.mem_incidentEdgeFinset_iff {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) (e : ↑G.edgeSet) : e ∈ G.incidentEdgeFinset v ↔ v ∈ ↑e

theorem SimpleGraph.convex_edmondsPolytope {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Convex ℝ G.edmondsPolytope

theorem SimpleGraph.pm_indicator_satisfies_degree {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (M : G.Subgraph) (hM : M.IsPerfectMatching) (v : V) : ∑ e ∈ G.incidentEdgeFinset v, (fun (e : ↑G.edgeSet) => if ↑e ∈ M.edgeSet then 1 else 0) e = 1

theorem SimpleGraph.pm_indicator_satisfies_oddset {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (M : G.Subgraph) (hM : M.IsPerfectMatching) (S : Finset V) (hS : Odd S.card) : ∑ e ∈ G.edgeCutFinset S, (fun (e : ↑G.edgeSet) => if ↑e ∈ M.edgeSet then 1 else 0) e ≥ 1

theorem SimpleGraph.pm_indicators_subset_edmondsPolytope {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : G.perfectMatchingIndicators ⊆ G.edmondsPolytope

theorem SimpleGraph.perfectMatchingPolytope_subset_edmondsPolytope {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : G.perfectMatchingPolytope ⊆ G.edmondsPolytope

theorem SimpleGraph.integral_edmondsPolytope_mem_pm {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (x : ↑G.edgeSet → ℝ) (hdeg : ∀ (v : V), ∑ e ∈ G.incidentEdgeFinset v, x e = 1) (hint : ∀ (e : ↑G.edgeSet), x e = 0 ∨ x e = 1) : x ∈ G.perfectMatchingIndicators

theorem SimpleGraph.mem_edgeCutFinset_iff {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) (e : ↑G.edgeSet) : e ∈ G.edgeCutFinset S ↔ ∃ a ∈ S, ∃ b ∉ S, ↑e = s(a, b)

theorem SimpleGraph.edgeCutFinset_singleton_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) : G.edgeCutFinset {v} = G.incidentEdgeFinset v

theorem SimpleGraph.nonintegral_has_tight_oddset {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (x : ↑G.edgeSet → ℝ) (hx : x ∈ G.edmondsPolytope) (heven : Even (Fintype.card V)) (hni : ∃ (e : ↑G.edgeSet), x e ≠ 0 ∧ x e ≠ 1) : ∃ (W : Finset V), Odd W.card ∧ ∑ e ∈ G.edgeCutFinset W, x e = 1

theorem SimpleGraph.edmondsPolytope_pm_decomposition_aux_local {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

theorem SimpleGraph.edmondsPolytope_subset_perfectMatchingPolytope {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (heven : Even (Fintype.card V)) : G.edmondsPolytope ⊆ G.perfectMatchingPolytope

theorem SimpleGraph.edmonds_perfect_matching_polytope {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (heven : Even (Fintype.card V)) : G.edmondsPolytope = G.perfectMatchingPolytope