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

theorem BipartiteMatchingPolytope.constraintMatrix_TU_of_bipartite {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq (Sym2 V)] (hG : G.IsBipartite) : ((SimpleGraph.incMatrix ℤ G).fromRows (-1)).IsTotallyUnimodular

def BipartiteMatchingPolytope.matchingLPRelaxation {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Set (Sym2 V → ℝ)

def BipartiteMatchingPolytope.matchingIndicators {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) : Set (Sym2 V → ℝ)

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

theorem BipartiteMatchingPolytope.matchingIndicators_subset_matchingLPRelaxation {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : matchingIndicators G ⊆ matchingLPRelaxation G

theorem BipartiteMatchingPolytope.convexHull_matchingIndicators_subset_matchingLPRelaxation {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : (convexHull ℝ) (matchingIndicators G) ⊆ matchingLPRelaxation G

theorem BipartiteMatchingPolytope.extremePoints_matchingLP_are_indicators (V : Type u_2) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.IsBipartite) : Set.extremePoints ℝ (matchingLPRelaxation G) ⊆ matchingIndicators G

theorem BipartiteMatchingPolytope.matchingLP_eq_convexHull_extremePoints (V : Type u_2) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.IsBipartite) : matchingLPRelaxation G ⊆ (convexHull ℝ) (Set.extremePoints ℝ (matchingLPRelaxation G))

theorem BipartiteMatchingPolytope.matchingLP_subset_convexHull_indicators (V : Type u_2) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.IsBipartite) : matchingLPRelaxation G ⊆ (convexHull ℝ) (matchingIndicators G)

theorem BipartiteMatchingPolytope.bipartite_matching_polytope_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.IsBipartite) : matchingLPRelaxation G = (convexHull ℝ) (matchingIndicators G)