Matchings represented by original edge positions

matchingOfPositions uses the original graph's adjacency and precisely the covered vertices; it represents an incomplete matching without adding isolated vertices to its vertex set. The position count is the cardinality of the existing Mathlib subgraph edge set.

def Cslib.Complexity.Graph.matchingOfPositions (G : Graph) (S : Finset ℕ) : G.induced.Subgraph

Keep the selected original edges and exactly their endpoints.

theorem Cslib.Complexity.Graph.isMatching_matchingOfPositions {G : Graph} {S : Finset ℕ} (huniq : ∀ v ∈ G.vertices, ∀ i ∈ S, ∀ j ∈ S, incident (G.edgeList.getD i (0, 0)) v = true → incident (G.edgeList.getD j (0, 0)) v = true → i = j) : (G.matchingOfPositions S).IsMatching

At most one selected incident position per vertex suffices for a Mathlib matching.

theorem Cslib.Complexity.Graph.positions_matchingOfPositions {G : Graph} {S : Finset ℕ} (hS : ∀ i ∈ S, i < G.edgeList.length) : positions (G.matchingOfPositions S) = S

Every selected valid edge is recovered by the represented subgraph.

theorem Cslib.Complexity.Graph.card_positions {G : Graph} (M : G.induced.Subgraph) : (positions M).card = M.edgeSet.ncard

Position cardinality is actual unoriented edge cardinality, for every subgraph.