structure RandomInjection.BipartiteMatching (X : Type u_3) (Y : Type u_4) [DecidableEq X] [DecidableEq Y] : Type (max u_3 u_4)

A bipartite matching between $X$ and $Y$: a finite set of edges $(x, y)$ in which no two distinct edges share a left endpoint or a right endpoint.

• edges : Finset (X × Y)
• left_injective ⦃e₁ e₂ : X × Y⦄ : e₁ ∈ self.edges → e₂ ∈ self.edges → e₁.1 = e₂.1 → e₁ = e₂
• right_injective ⦃e₁ e₂ : X × Y⦄ : e₁ ∈ self.edges → e₂ ∈ self.edges → e₁.2 = e₂.2 → e₁ = e₂

def RandomInjection.BipartiteMatching.leftVertices {X : Type u_1} {Y : Type u_2} [DecidableEq X] [DecidableEq Y] (F : BipartiteMatching X Y) : Finset X

The set of left vertices covered by the bipartite matching $F$.

def RandomInjection.BipartiteMatching.rightVertices {X : Type u_1} {Y : Type u_2} [DecidableEq X] [DecidableEq Y] (F : BipartiteMatching X Y) : Finset Y

The set of right vertices covered by the bipartite matching $F$.

def RandomInjection.BipartiteMatching.IsComplete {X : Type u_1} {Y : Type u_2} [DecidableEq X] [DecidableEq Y] [Fintype X] (M : BipartiteMatching X Y) : Prop

A bipartite matching is complete (a perfect matching from $X$) if every left vertex is covered.

def RandomInjection.VertexDisjoint {X : Type u_1} {Y : Type u_2} [DecidableEq X] [DecidableEq Y] (F₁ F₂ : BipartiteMatching X Y) : Prop

Two bipartite matchings are vertex-disjoint if their left vertex sets and their right vertex sets are both disjoint.

def RandomInjection.CanonicalNegDepGraph {X : Type u_1} {Y : Type u_2} [DecidableEq X] [DecidableEq Y] {n : ℕ} (F : Fin n → BipartiteMatching X Y) : SimpleGraph (Fin n)

Canonical dependency graph for a family $(F_i)$ of matchings (Setup 6.5.4): vertices are the indices, and $i, j$ are adjacent when they are distinct and the matchings $F_i, F_j$ share a left or right endpoint.