def Matroid.IsMatching {α : Type u_1} {β : Type u_2} (Adj : α → β → Prop) (f : β → α) (I : Set α) (J : Set β) : Prop

Equations

• Matroid.IsMatching Adj f I J = (Set.BijOn f J I ∧ ∀ v ∈ J, Adj (f v) v)

theorem Matroid.IsMatching.adj {α : Type u_1} {β : Type u_2} {Adj : α → β → Prop} {f : β → α} {v : β} {I₀ : Set α} {I : Set β} (h : IsMatching Adj f I₀ I) (hv : v ∈ I) : Adj (f v) v

theorem Matroid.IsMatching.bijOn {α : Type u_1} {β : Type u_2} {Adj : α → β → Prop} {f : β → α} {I₀ : Set α} {I : Set β} (h : IsMatching Adj f I₀ I) : Set.BijOn f I I₀

theorem Matroid.IsMatching.card_eq {α : Type u_1} {β : Type u_2} {Adj : α → β → Prop} {f : β → α} {I₀ : Finset α} {I : Finset β} (h : IsMatching Adj f ↑I₀ ↑I) : I₀.card = I.card

def Matroid.AdjIndep {α : Type u_1} {β : Type u_2} (M : Matroid α) (Adj : α → β → Prop) (I : Finset β) : Prop

I : Finset β is AdjIndep relative to M : Matroid α and Adj : α → β → Prop if I is matchable to an M-independent set using edges in Adj.

Equations

• M.AdjIndep Adj I = (I = ∅ ∨ ∃ (I₀ : Finset α) (f : β → α), M.Indep ↑I₀ ∧ Matroid.IsMatching Adj f ↑I₀ ↑I)

theorem Matroid.AdjIndep.exists {α : Type u_1} {β : Type u_2} {M : Matroid α} {Adj : α → β → Prop} [Nonempty α] {I : Finset β} (h : M.AdjIndep Adj I) : ∃ (I₀ : Finset α) (f : β → α), M.Indep ↑I₀ ∧ IsMatching Adj f ↑I₀ ↑I

theorem Matroid.AdjIndep.subset {α : Type u_1} {β : Type u_2} {M : Matroid α} {Adj : α → β → Prop} {I J : Finset β} (hI : M.AdjIndep Adj I) (hJI : J ⊆ I) : M.AdjIndep Adj J

theorem Matroid.AdjIndep.augment {α : Type u_1} {β : Type u_2} {M : Matroid α} {Adj : α → β → Prop} {I J : Finset β} [DecidableEq β] (hI : M.AdjIndep Adj I) (hJ : M.AdjIndep Adj J) (hIJ : I.card < J.card) : ∃ e ∈ J, e ∉ I ∧ M.AdjIndep Adj (insert e I)

def Matroid.adjMap {α : Type u_1} {β : Type u_2} [DecidableEq β] (M : Matroid α) (Adj : α → β → Prop) (E : Set β) : Matroid β

Given M : Matroid α and a graph H with bipartition (α, β) described by an adjacency predicate Adj : α → β → Prop, M.adjMap Adj E is the finitary matroid on β with ground set E whose finite independent sets are those H-matchable to an independent set of M. This doesn't require M to be finitary to be well-defined, but only depends on the collection of finite independent sets of M. This construction fails to be a matroid if we try to allow infinite sets to be independent; see the docstring of Data.Matroid.Map.

Equations

• M.adjMap Adj E = (IndepMatroid.ofFinset Set.univ (M.AdjIndep Adj) ⋯ ⋯ ⋯ ⋯).matroid.restrict E

@[simp]

theorem Matroid.adjMap_indep_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] (M : Matroid α) (Adj : α → β → Prop) (E : Set β) {I : Finset β} : (M.adjMap Adj E).Indep ↑I ↔ M.AdjIndep Adj I ∧ ↑I ⊆ E

@[simp]

theorem Matroid.adjMap_ground_eq {α : Type u_1} {β : Type u_2} [DecidableEq β] (M : Matroid α) (Adj : α → β → Prop) (E : Set β) : (M.adjMap Adj E).E = E

instance Matroid.instFinitaryAdjMap {α : Type u_1} {β : Type u_2} [DecidableEq β] (M : Matroid α) (Adj : α → β → Prop) (E : Set β) : (M.adjMap Adj E).Finitary

M.adjMap Adj E is finitary.