class Matroid.SupportClass (γ : Type u → Sort u') : Sort (max (u + 2) u')

Matroid.SupportClass γ means that for M : Matroid α, terms of type γ α have a notion of 'supported' that depends only on the ground set of M. For sets, this is containment in M.E, and for elements, this is membership in M.E.

• supported {α : Type u} : Matroid α → γ α → Prop
• congr {α : Type u} {M M' : Matroid α} : M.E = M'.E → ∀ (X : γ α), supported M X ↔ supported M' X

@[instance_reducible]

instance Matroid.SupportClass.pure {μ : Sort u'} : Matroid.SupportClass fun (x : Type u_1) => μ

Supportedness of a pure sort. (Everything is supported.)

Equations

• Matroid.SupportClass.pure = { supported := fun {α : Type ?u.1} (M : Matroid α) (X : μ) => True, congr := ⋯ }

@[simp]

theorem Matroid.SupportClass.supported_pure {α : Type u} {μ : Sort u'} {M : Matroid α} {X : μ} : supported M X

@[instance_reducible]

instance Matroid.SupportClass.list : Matroid.SupportClass List

Supportedness of lists.

Equations

• Matroid.SupportClass.list = { supported := fun {α : Type ?u.1} (M : Matroid α) (X : List α) => ∀ e ∈ X, e ∈ M.E, congr := @Matroid.SupportClass.list._proof_1 }

@[simp]

theorem Matroid.SupportClass.list_supported {α✝ : Type u_1} (M : Matroid α✝) (X : List α✝) : supported M X = ∀ e ∈ X, e ∈ M.E

@[instance_reducible]

instance Matroid.SupportClass.id : Matroid.SupportClass id

Supportedness of elements.

Equations

• Matroid.SupportClass.id = { supported := fun {α : Type ?u.1} (M : Matroid α) (x : id α) => x ∈ M.E, congr := @Matroid.SupportClass.id._proof_1 }

@[simp]

theorem Matroid.SupportClass.id_supported {α✝ : Type u_1} (M : Matroid α✝) (x : id α✝) : supported M x = (x ∈ M.E)

@[instance_reducible]

instance Matroid.SupportClass.set : Matroid.SupportClass Set

Supportedness of sets.

Equations

• Matroid.SupportClass.set = { supported := fun {α : Type ?u.1} (M : Matroid α) (X : Set α) => X ⊆ M.E, congr := @Matroid.SupportClass.set._proof_1 }

@[simp]

theorem Matroid.SupportClass.set_supported {α✝ : Type u_1} (M : Matroid α✝) (X : Set α✝) : supported M X = (X ⊆ M.E)

@[instance_reducible]

instance Matroid.SupportClass.toSet (γ : Type u_1 → Type u_2) [hγ : Matroid.SupportClass γ] : Matroid.SupportClass fun (α : Type u_1) => Set (γ α)

Supportedness of sets of supported types.

Equations

• Matroid.SupportClass.toSet γ = { supported := fun {α : Type ?u.2} (M : Matroid α) (s : Set (γ α)) => ∀ x ∈ s, Matroid.SupportClass.supported M x, congr := ⋯ }

@[simp]

theorem Matroid.SupportClass.toSet_supported (γ : Type u_1 → Type u_2) [hγ : Matroid.SupportClass γ] {α✝ : Type u_1} (M : Matroid α✝) (s : Set (γ α✝)) : supported M s = ∀ x ∈ s, supported M x

@[instance_reducible]

instance Matroid.SupportClass.toFun {ι : Type u_1} {γ : Type u_2 → Type u_3} [hγ : Matroid.SupportClass γ] : Matroid.SupportClass fun (α : Type u_2) => ι → γ α

Supportedness of tuples of supported types.

Equations

• Matroid.SupportClass.toFun = { supported := fun {α : Type ?u.2} (M : Matroid α) (X : ι → γ α) => ∀ (i : ι), Matroid.SupportClass.supported M (X i), congr := ⋯ }

@[simp]

theorem Matroid.SupportClass.toFun_supported {ι : Type u_1} {γ : Type u_2 → Type u_3} [hγ : Matroid.SupportClass γ] {α✝ : Type u_2} (M : Matroid α✝) (X : ι → γ α✝) : supported M X = ∀ (i : ι), supported M (X i)

@[instance_reducible]

instance Matroid.SupportClass.toList {γ : Type u_1 → Type u_2} [hγ : Matroid.SupportClass γ] : Matroid.SupportClass fun (α : Type u_1) => List (γ α)

Supportedness of lists of supported types.

Equations

• Matroid.SupportClass.toList = { supported := fun {α : Type ?u.2} (M : Matroid α) (L : List (γ α)) => ∀ x ∈ L, Matroid.SupportClass.supported M x, congr := ⋯ }

@[simp]

theorem Matroid.SupportClass.toList_supported {γ : Type u_1 → Type u_2} [hγ : Matroid.SupportClass γ] {α✝ : Type u_1} (M : Matroid α✝) (L : List (γ α✝)) : supported M L = ∀ x ∈ L, supported M x

class Matroid.TransferClass (γ : Type u → Sort u') (δ : Type v → Sort v') [Sγ : Matroid.SupportClass γ] [Sδ : Matroid.SupportClass δ] : Sort (max (max (max (u + 2) u') (v + 2)) v')

Matroid.TransferClass γ δ contains the data needed to move terms of type γ α to ones of type δ β via a function f : α → β. Transferred values need to respect supportedness in a given matroid.

• transfer {α : Type u} {β : Type v} : (α → β) → γ α → δ β
• transferEmpty {α : Type u} {β : Type v} : IsEmpty β → (x : γ α) → SupportClass.supported (emptyOn α) x → δ β
• supported_transfer ⦃α : Type u⦄ ⦃β : Type v⦄ ⦃M : Matroid α⦄ ⦃f : α → β⦄ (hf : Set.InjOn f M.E) ⦃x : γ α⦄ : SupportClass.supported M x → SupportClass.supported (M.map f hf) (transfer f x)
• supported_transferEmpty ⦃α : Type u⦄ ⦃β : Type v⦄ (hβ : IsEmpty β) (x : γ α) (hx : SupportClass.supported (emptyOn α) x) : SupportClass.supported (emptyOn β) (transferEmpty hβ x hx)

@[instance_reducible]

instance Matroid.TransferClass.pure {μ : Sort u'} : Matroid.TransferClass (fun (x : Type u_1) => μ) fun (x : Type u_2) => μ

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matroid.TransferClass.pure_transfer {μ : Sort u'} {α✝ : Type u_1} {β✝ : Type u_2} (x✝ : α✝ → β✝) (x : μ) : transfer x✝ x = x

@[simp]

theorem Matroid.TransferClass.pure_transferEmpty {μ : Sort u'} {α✝ : Type u_1} {β✝ : Type u_2} (x✝ : IsEmpty β✝) (x : μ) (x✝¹ : SupportClass.supported (emptyOn α✝) x) : transferEmpty x✝ x x✝¹ = x

@[instance_reducible]

instance Matroid.TransferClass.id : Matroid.TransferClass id id

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matroid.TransferClass.id_transferEmpty {α✝ : Type u_1} {β✝ : Type u_2} (x✝ : IsEmpty β✝) (x✝¹ : id α✝) (h : SupportClass.supported (emptyOn α✝) x✝¹) : transferEmpty x✝ x✝¹ h = ⋯.elim

@[simp]

theorem Matroid.TransferClass.id_transfer {α✝ : Type u_1} {β✝ : Type u_2} (a : α✝ → β✝) (a✝ : α✝) : transfer a a✝ = id a a✝

@[instance_reducible]

instance Matroid.TransferClass.set : Matroid.TransferClass Set Set

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matroid.TransferClass.set_transfer {α✝ : Type u_1} {β✝ : Type u_2} (f : α✝ → β✝) (s : Set α✝) : transfer f s = f '' s

@[simp]

theorem Matroid.TransferClass.set_transferEmpty {α✝ : Type u_1} {β✝ : Type u_2} (x✝ : IsEmpty β✝) (x✝¹ : Set α✝) (x✝² : SupportClass.supported (emptyOn α✝) x✝¹) : transferEmpty x✝ x✝¹ x✝² = ∅

@[instance_reducible]

instance Matroid.TransferClass.list : Matroid.TransferClass List List

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matroid.TransferClass.list_transferEmpty {α✝ : Type u_1} {β✝ : Type u_2} (x✝ : IsEmpty β✝) (x✝¹ : List α✝) (x✝² : SupportClass.supported (emptyOn α✝) x✝¹) : transferEmpty x✝ x✝¹ x✝² = []

@[simp]

theorem Matroid.TransferClass.list_transfer {α✝ : Type u_1} {β✝ : Type u_2} (f : α✝ → β✝) (X : List α✝) : transfer f X = List.map f X

@[instance_reducible]

instance Matroid.TransferClass.toSet {γ : Type u_1 → Type u_2} {δ : Type u_3 → Type u_4} [Sγ : Matroid.SupportClass γ] [Sδ : Matroid.SupportClass δ] [T : Matroid.TransferClass γ δ] : Matroid.TransferClass (fun (α : Type u_1) => Set (γ α)) fun (β : Type u_3) => Set (δ β)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matroid.TransferClass.toSet_transfer {γ : Type u_1 → Type u_2} {δ : Type u_3 → Type u_4} [Sγ : Matroid.SupportClass γ] [Sδ : Matroid.SupportClass δ] [T : Matroid.TransferClass γ δ] {α✝ : Type u_1} {β✝ : Type u_3} (f : α✝ → β✝) (X : Set (γ α✝)) : transfer f X = transfer f '' X

@[simp]

theorem Matroid.TransferClass.toSet_transferEmpty {γ : Type u_1 → Type u_2} {δ : Type u_3 → Type u_4} [Sγ : Matroid.SupportClass γ] [Sδ : Matroid.SupportClass δ] [T : Matroid.TransferClass γ δ] (α : Type u_1) (β : Type u_3) (hβ : IsEmpty β) (X : Set (γ α)) (hX : SupportClass.supported (emptyOn α) X) : transferEmpty hβ X hX = {y : δ β | ∃ (x : γ α) (_ : x ∈ X) (hx : SupportClass.supported (emptyOn α) x), transferEmpty hβ x hx = y}

@[instance_reducible]

instance Matroid.TransferClass.toList {γ : Type u_1 → Type u_2} {δ : Type u_3 → Type u_4} [Sγ : Matroid.SupportClass γ] [Sδ : Matroid.SupportClass δ] [T : Matroid.TransferClass γ δ] : Matroid.TransferClass (fun (α : Type u_1) => List (γ α)) fun (β : Type u_3) => List (δ β)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matroid.TransferClass.toList_transfer {γ : Type u_1 → Type u_2} {δ : Type u_3 → Type u_4} [Sγ : Matroid.SupportClass γ] [Sδ : Matroid.SupportClass δ] [T : Matroid.TransferClass γ δ] {α✝ : Type u_1} {β✝ : Type u_3} (f : α✝ → β✝) (X : List (γ α✝)) : transfer f X = List.map (transfer f) X

@[simp]

theorem Matroid.TransferClass.toList_transferEmpty {γ : Type u_1 → Type u_2} {δ : Type u_3 → Type u_4} [Sγ : Matroid.SupportClass γ] [Sδ : Matroid.SupportClass δ] [T : Matroid.TransferClass γ δ] {α✝ : Type u_1} {β✝ : Type u_3} (hβ : IsEmpty β✝) (L : List (γ α✝)) (hL : SupportClass.supported (emptyOn α✝) L) : transferEmpty hβ L hL = List.pmap (transferEmpty hβ) L hL

@[instance_reducible]

instance Matroid.TransferClass.toFun {γ : Type u_1 → Type u_2} {δ : Type u_3 → Type u_4} {ι : Type u_5} [hγ : Matroid.SupportClass γ] [Matroid.SupportClass δ] [T : Matroid.TransferClass γ δ] : Matroid.TransferClass (fun (α : Type u_1) => ι → γ α) fun (β : Type u_3) => ι → δ β

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matroid.TransferClass.toFun_transferEmpty {γ : Type u_1 → Type u_2} {δ : Type u_3 → Type u_4} {ι : Type u_5} [hγ : Matroid.SupportClass γ] [Matroid.SupportClass δ] [T : Matroid.TransferClass γ δ] {α✝ : Type u_1} {β✝ : Type u_3} (hβ : IsEmpty β✝) (x : ι → γ α✝) (hx : SupportClass.supported (emptyOn α✝) x) (i : ι) : transferEmpty hβ x hx i = transferEmpty hβ (x i) ⋯

@[simp]

theorem Matroid.TransferClass.toFun_transfer_eq {γ : Type u → Type u'} {δ : Type v → Type v'} {ι : Type u_1} [hγ : Matroid.SupportClass γ] [Matroid.SupportClass δ] [T : Matroid.TransferClass γ δ] {α : Type u} {β : Type v} {f : α → β} {X : ι → γ α} : transfer f X = fun (i : ι) => transfer f (X i)

class Matroid.GroundedFun {γ : Type u → Sort u'} [S : Matroid.SupportClass γ] (F : {α : Type u} → Matroid α → γ α) : Prop

A function from matroids is grounded if it always takes values in the ground set.

• supported ⦃α : Type u⦄ (M : Matroid α) : SupportClass.supported M (F M)

class Matroid.GroundedFun₂ {γ : Type u → Sort u_1} {γ' : Type u → Sort u_2} [S : Matroid.SupportClass γ] [S' : Matroid.SupportClass γ'] (F : {α : Type u} → Matroid α → γ α → γ' α) : Prop

• supported ⦃α : Type u⦄ (M : Matroid α) (x : γ α) : SupportClass.supported M x → SupportClass.supported M (F M x)

instance Matroid.instGroundedFun {μ : Type w} (F : {α : Type u_1} → Matroid α → μ) : GroundedFun fun {α : Type u_1} => F

instance Matroid.instGroundedFun₂ {γ : Type u → Sort u_1} {μ : Sort u_2} [Matroid.SupportClass γ] (F : {α : Type u} → Matroid α → γ α → μ) : GroundedFun₂ fun {α : Type u} => F

instance Matroid.instGroundedFun₂SetClosure : GroundedFun₂ fun {α : Type u_1} => closure

class Matroid.GroundedPred {γ : Type u → Sort u'} [S : Matroid.SupportClass γ] (P : {α : Type u} → Matroid α → γ α → Prop) : Prop

A predicate of type γ α → Prop is a GroundedPred if it is only true for elements of γ α that are supported by M.

• supported ⦃α : Type u⦄ ⦃M : Matroid α⦄ ⦃x : γ α⦄ : P M x → SupportClass.supported M x

class Matroid.GroundedPred₂ {γ₁ : Type u → Sort u₁} {γ₂ : Type u → Sort u₂} [S₁ : Matroid.SupportClass γ₁] [S₂ : Matroid.SupportClass γ₂] (P : {α : Type u} → Matroid α → γ₁ α → γ₂ α → Prop) : Prop

• supported ⦃α : Type u⦄ ⦃M : Matroid α⦄ ⦃x : γ₁ α⦄ ⦃y : γ₂ α⦄ : P M x y → SupportClass.supported M x ∧ SupportClass.supported M y

instance Matroid.instGroundedPredSetIndep : GroundedPred fun {α : Type u_1} => Indep

instance Matroid.instGroundedPredSetDep : GroundedPred fun {α : Type u_1} => Dep

instance Matroid.instGroundedPredSetIsBase : GroundedPred fun {α : Type u_1} => IsBase

instance Matroid.instGroundedPredSetSpanning : GroundedPred fun {α : Type u_1} => Spanning

instance Matroid.instGroundedPredSetNonspanning : GroundedPred fun {α : Type u_1} => Nonspanning

instance Matroid.instGroundedPredSetCoindep : GroundedPred fun {α : Type u_1} => Coindep

instance Matroid.instGroundedPredSetCodep : GroundedPred fun {α : Type u_1} => Codep

instance Matroid.instGroundedPred₂SetIsBasis : GroundedPred₂ fun {α : Type u_1} => IsBasis

class Matroid.Invariant {γ : Type u_1 → Sort u_2} {δ : Type u_3 → Sort u_4} [S : Matroid.SupportClass γ] [T : Matroid.SupportClass δ] [C : Matroid.TransferClass γ δ] (F : {α : Type u_1} → Matroid α → γ α) (G : {β : Type u_3} → Matroid β → δ β) : Prop

• map_eq ⦃α : Type u_1⦄ ⦃β : Type u_3⦄ ⦃M : Matroid α⦄ ⦃f : α → β⦄ (h : Set.InjOn f M.E) : TransferClass.transfer f (F M) = G (M.map f h)

theorem Matroid.Invariant.and (P P' : {α : Type u} → Matroid α → Prop) (Q Q' : {α : Type v} → Matroid α → Prop) [h : Invariant (fun {α : Type u} => P) fun {β : Type v} => Q] [h' : Invariant (fun {α : Type u} => P') fun {β : Type v} => Q'] : Invariant (fun {α : Type u} (M : Matroid α) => P M ∧ P' M) fun {β : Type v} (M : Matroid β) => Q M ∧ Q' M

class Matroid.InvariantFun {γ₁ : Type u → Sort u₁} {γ₂ : Type u → Sort u₂} {δ₁ : Type v → Sort v₁} {δ₂ : Type v → Sort v₂} [S₁ : Matroid.SupportClass γ₁] [S₂ : Matroid.SupportClass γ₂] [T₁ : Matroid.SupportClass δ₁] [T₂ : Matroid.SupportClass δ₂] [C₁ : Matroid.TransferClass γ₁ δ₁] [C₂ : Matroid.TransferClass γ₂ δ₂] (F : {α : Type u} → Matroid α → γ₁ α → γ₂ α) (G : {β : Type v} → Matroid β → δ₁ β → δ₂ β) : Prop

• of_empty ⦃α : Type u⦄ ⦃β : Type v⦄ (hβ : IsEmpty β) ⦃x : γ₁ α⦄ (hx : SupportClass.supported (emptyOn α) x) (hx' : SupportClass.supported (emptyOn α) (F (emptyOn α) x)) : TransferClass.transferEmpty hβ (F (emptyOn α) x) hx' = G (emptyOn β) (TransferClass.transferEmpty hβ x hx)
• map_eq ⦃α : Type u⦄ ⦃β : Type v⦄ ⦃M : Matroid α⦄ ⦃f : α → β⦄ (hf : Set.InjOn f M.E) ⦃x : γ₁ α⦄ : SupportClass.supported M x → TransferClass.transfer f (F M x) = G (M.map f hf) (TransferClass.transfer f x)

class Matroid.InvariantFun₂ {γ₁ : Type u → Sort u₁} {γ₂ : Type u → Sort u₂} {δ₁ : Type v → Sort v₁} {δ₂ : Type v → Sort v₂} {μ : Sort w} [S₁ : Matroid.SupportClass γ₁] [T₁ : Matroid.SupportClass δ₁] [C₁ : Matroid.TransferClass γ₁ δ₁] [S₂ : Matroid.SupportClass γ₂] [T₂ : Matroid.SupportClass δ₂] [C₂ : Matroid.TransferClass γ₂ δ₂] (F : {α : Type u} → Matroid α → γ₁ α → γ₂ α → μ) (G : {β : Type v} → Matroid β → δ₁ β → δ₂ β → μ) : Prop

This could be generalized further like InvariantFun, allowing the output type to take values in a sort depending on the matroid type

• of_empty ⦃α : Type u⦄ ⦃β : Type v⦄ (hβ : IsEmpty β) ⦃x : γ₁ α⦄ ⦃x' : γ₂ α⦄ (hx : SupportClass.supported (emptyOn α) x) (hx' : SupportClass.supported (emptyOn α) x') : F (emptyOn α) x x' = G (emptyOn β) (TransferClass.transferEmpty hβ x hx) (TransferClass.transferEmpty hβ x' hx')
• map_eq ⦃α : Type u⦄ ⦃β : Type v⦄ ⦃M : Matroid α⦄ ⦃f : α → β⦄ (hf : Set.InjOn f M.E) ⦃x : γ₁ α⦄ ⦃x' : γ₂ α⦄ : SupportClass.supported M x → SupportClass.supported M x' → F M x x' = G (M.map f hf) (TransferClass.transfer f x) (TransferClass.transfer f x')

instance Matroid.InvariantFun.inst {μ : Sort u_7} {μ' : Sort u_8} {f : μ → μ'} : InvariantFun (fun {α : Type u_9} (x : Matroid α) => f) fun {β : Type u_10} (x : Matroid β) => f

theorem Matroid.InvariantFun.map_pure_eq {α : Type u} {β : Type v} {γ₁ : Type u → Sort u_1} {δ₁ : Type v → Sort u_4} {μ : Sort u_7} [S₁ : Matroid.SupportClass γ₁] [T₁ : Matroid.SupportClass δ₁] [C₁ : Matroid.TransferClass γ₁ δ₁] (F : {α : Type u} → Matroid α → γ₁ α → μ) (G : {β : Type v} → Matroid β → δ₁ β → μ) [h : InvariantFun (fun {α : Type u} => F) fun {β : Type v} => G] {M : Matroid α} {f : α → β} {hf : Set.InjOn f M.E} {x : γ₁ α} (hx : SupportClass.supported M x) : G (M.map f hf) (TransferClass.transfer f x) = F M x

theorem Matroid.InvariantFun.comp_right' {γ₁ : Type u → Sort u_1} {γ₂ : Type u → Sort u_2} {γ₃ : Type u → Sort u_3} {δ₁ : Type v → Sort u_4} {δ₂ : Type v → Sort u_5} {δ₃ : Type v → Sort u_6} [S₁ : Matroid.SupportClass γ₁] [S₂ : Matroid.SupportClass γ₂] [S₃ : Matroid.SupportClass γ₃] [T₁ : Matroid.SupportClass δ₁] [T₂ : Matroid.SupportClass δ₂] [T₃ : Matroid.SupportClass δ₃] [C₁ : Matroid.TransferClass γ₁ δ₁] [C₂ : Matroid.TransferClass γ₂ δ₂] [C₃ : Matroid.TransferClass γ₃ δ₃] (F : {α : Type u} → Matroid α → γ₁ α → γ₂ α) (G : {β : Type v} → Matroid β → δ₁ β → δ₂ β) [h : InvariantFun (fun {α : Type u} => F) fun {β : Type v} => G] [hF : GroundedFun₂ fun {α : Type u} => F] (s : {α : Type u} → Matroid α → γ₂ α → γ₃ α) (t : {β : Type v} → Matroid β → δ₂ β → δ₃ β) [hst : InvariantFun (fun {α : Type u} => s) fun {β : Type v} => t] : InvariantFun (fun {α : Type u} (M : Matroid α) (x : γ₁ α) => s M (F M x)) fun {β : Type v} (N : Matroid β) (y : δ₁ β) => t N (G N y)

theorem Matroid.InvariantFun.comp_right {γ₁ : Type u → Sort u_1} {δ₁ : Type v → Sort u_4} [S₁ : Matroid.SupportClass γ₁] [T₁ : Matroid.SupportClass δ₁] [C₁ : Matroid.TransferClass γ₁ δ₁] {μ : Sort u_9} {μ' : Sort u_10} (F : {α : Type u} → Matroid α → γ₁ α → μ) (G : {β : Type v} → Matroid β → δ₁ β → μ) [h : InvariantFun (fun {α : Type u} => F) fun {β : Type v} => G] (s : μ → μ') : InvariantFun (fun {α : Type u} (M : Matroid α) (x : γ₁ α) => s (F M x)) fun {β : Type v} (N : Matroid β) (y : δ₁ β) => s (G N y)

theorem Matroid.InvariantFun.comp_left {γ₁ : Type u → Sort u_1} {γ₂ : Type u → Sort u_2} {δ₁ : Type v → Sort u_4} {δ₂ : Type v → Sort u_5} [S₁ : Matroid.SupportClass γ₁] [S₂ : Matroid.SupportClass γ₂] [T₁ : Matroid.SupportClass δ₁] [T₂ : Matroid.SupportClass δ₂] [C₁ : Matroid.TransferClass γ₁ δ₁] [C₂ : Matroid.TransferClass γ₂ δ₂] {γ₁' : Type u → Sort u_9} {δ₁' : Type v → Sort u_10} [S₁' : Matroid.SupportClass γ₁'] [T₁' : Matroid.SupportClass δ₁'] [C₁' : Matroid.TransferClass γ₁' δ₁'] (F : {α : Type u} → Matroid α → γ₁ α → γ₂ α) (G : {β : Type v} → Matroid β → δ₁ β → δ₂ β) [h : InvariantFun (fun {α : Type u} => F) fun {β : Type v} => G] (a : {α : Type u} → Matroid α → γ₁' α → γ₁ α) (b : {β : Type v} → Matroid β → δ₁' β → δ₁ β) (ha : ∀ {α : Type u} (M : Matroid α) (x : γ₁' α), SupportClass.supported M x → SupportClass.supported M (a M x)) (hab0 : ∀ {α : Type u} {β : Type v} (hβ : IsEmpty β) (x : γ₁' α) (hx : SupportClass.supported (emptyOn α) x), TransferClass.transferEmpty hβ (a (emptyOn α) x) ⋯ = b (emptyOn β) (TransferClass.transferEmpty hβ x hx)) (hab : ∀ {α : Type u} {β : Type v} (M : Matroid α) (f : α → β) (hf : Set.InjOn f M.E) (x : γ₁' α), SupportClass.supported M x → TransferClass.transfer f (a M x) = b (M.map f hf) (TransferClass.transfer f x)) : InvariantFun (fun {α : Type u} (M : Matroid α) (X : γ₁' α) => F M (a M X)) fun {β : Type v} (N : Matroid β) (Y : δ₁' β) => G N (b N Y)

theorem Matroid.InvariantFun.combine {γ₁ : Type u → Sort u_1} {δ₁ : Type v → Sort u_4} {μ : Sort u_7} [S₁ : Matroid.SupportClass γ₁] [T₁ : Matroid.SupportClass δ₁] [C₁ : Matroid.TransferClass γ₁ δ₁] (F F' : {α : Type u} → Matroid α → γ₁ α → μ) (G G' : {β : Type v} → Matroid β → δ₁ β → μ) [h : InvariantFun (fun {α : Type u} => F) fun {β : Type v} => G] [h' : InvariantFun (fun {α : Type u} => F') fun {β : Type v} => G'] (φ : μ → μ → μ) : InvariantFun (fun {α : Type u} (M : Matroid α) (x : γ₁ α) => φ (F M x) (F' M x)) fun {β : Type v} (N : Matroid β) (x : δ₁ β) => φ (G N x) (G' N x)

theorem Matroid.InvariantFun.dual {γ₁ : Type u → Sort u_1} {γ₂ : Type u → Sort u_2} {δ₁ : Type v → Sort u_4} {δ₂ : Type v → Sort u_5} [S₁ : Matroid.SupportClass γ₁] [S₂ : Matroid.SupportClass γ₂] [T₁ : Matroid.SupportClass δ₁] [T₂ : Matroid.SupportClass δ₂] [C₁ : Matroid.TransferClass γ₁ δ₁] [C₂ : Matroid.TransferClass γ₂ δ₂] (F : {α : Type u} → Matroid α → γ₁ α → γ₂ α) (G : {β : Type v} → Matroid β → δ₁ β → δ₂ β) [h : InvariantFun (fun {α : Type u} => F) fun {β : Type v} => G] : InvariantFun (fun {α : Type u} (M : Matroid α) (X : γ₁ α) => F M✶ X) fun {β : Type v} (N : Matroid β) (Y : δ₁ β) => G N✶ Y

theorem Matroid.InvariantFun.compl {γ₂ : Type u → Sort u_2} {δ₂ : Type v → Sort u_5} [S₂ : Matroid.SupportClass γ₂] [T₂ : Matroid.SupportClass δ₂] [C₂ : Matroid.TransferClass γ₂ δ₂] (F : {α : Type u} → Matroid α → Set α → γ₂ α) (G : {β : Type v} → Matroid β → Set β → δ₂ β) [h : InvariantFun (fun {α : Type u} => F) fun {β : Type v} => G] : InvariantFun (fun {α : Type u} (M : Matroid α) (X : Set α) => F M (M.E \ X)) fun {β : Type v} (N : Matroid β) (Y : Set β) => G N (N.E \ Y)

theorem Matroid.InvariantFun.encard : InvariantFun (fun {α : Type u} (x : Matroid α) (X : Set α) => X.encard) fun {β : Type v} (x : Matroid β) (Y : Set β) => Y.encard

theorem Matroid.InvariantFun.iff_ext {γ₁ : Type u → Sort u_1} {γ₂ : Type u → Sort u_2} {δ₁ : Type v → Sort u_4} {δ₂ : Type v → Sort u_5} [S₁ : Matroid.SupportClass γ₁] [S₂ : Matroid.SupportClass γ₂] [T₁ : Matroid.SupportClass δ₁] [T₂ : Matroid.SupportClass δ₂] [C₁ : Matroid.TransferClass γ₁ δ₁] [C₂ : Matroid.TransferClass γ₂ δ₂] (F : {α : Type u} → Matroid α → γ₁ α → γ₂ α) (G : {β : Type v} → Matroid β → δ₁ β → δ₂ β) : (InvariantFun (fun {α : Type u} => F) fun {β : Type v} => G) ↔ InvariantFun (fun {α : Type u} (M : Matroid α) (x : γ₁ α) => F M x) fun {β : Type v} (N : Matroid β) (y : δ₁ β) => G N y

theorem Matroid.InvariantFun.map {α : Type u} {β : Type v} {γ₁ : Type u → Sort u_1} {δ₁ : Type v → Sort u_4} [S₁ : Matroid.SupportClass γ₁] [T₁ : Matroid.SupportClass δ₁] [C₁ : Matroid.TransferClass γ₁ δ₁] {P : {α : Type u} → Matroid α → γ₁ α → Prop} {Q : {β : Type v} → Matroid β → δ₁ β → Prop} [h : InvariantFun (fun {α : Type u} => P) fun {β : Type v} => Q] [hP : GroundedPred fun {α : Type u} => P] {M : Matroid α} {f : α → β} {x : γ₁ α} (hx : P M x) (hf : Set.InjOn f M.E) : Q (M.map f hf) (TransferClass.transfer f x)

theorem Matroid.InvariantFun.map_iff {α : Type u} {β : Type v} {γ₁ : Type u → Sort u_1} {δ₁ : Type v → Sort u_4} [S₁ : Matroid.SupportClass γ₁] [T₁ : Matroid.SupportClass δ₁] [C₁ : Matroid.TransferClass γ₁ δ₁] {P : {α : Type u} → Matroid α → γ₁ α → Prop} {Q : {β : Type v} → Matroid β → δ₁ β → Prop} [h : InvariantFun (fun {α : Type u} => P) fun {β : Type v} => Q] {M : Matroid α} {f : α → β} {x : γ₁ α} (hf : Set.InjOn f M.E) (hx : SupportClass.supported M x) : Q (M.map f hf) (TransferClass.transfer f x) ↔ P M x

theorem Matroid.InvariantFun.map_elem_iff {α : Type u} {β : Type v} {P : {α : Type u} → Matroid α → α → Prop} {Q : {α : Type v} → Matroid α → α → Prop} [h : InvariantFun (fun {α : Type u} => P) fun {β : Type v} => Q] {M : Matroid α} {f : α → β} {x : α} (hf : Set.InjOn f M.E) (hx : x ∈ M.E) : Q (M.map f hf) (f x) ↔ P M x

theorem Matroid.InvariantFun.map_set {α : Type u} {β : Type v} {P : {α : Type u} → Matroid α → Set α → Prop} {Q : {β : Type v} → Matroid β → Set β → Prop} [h : InvariantFun (fun {α : Type u} => P) fun {β : Type v} => Q] [hP : GroundedPred fun {α : Type u} => P] {M : Matroid α} {f : α → β} {x : Set α} (hx : P M x) (hf : Set.InjOn f M.E) : Q (M.map f hf) (f '' x)

theorem Matroid.InvariantFun.map_elem {α : Type u} {β : Type v} {P : {α : Type u} → Matroid α → α → Prop} {Q : {β : Type v} → Matroid β → β → Prop} [h : InvariantFun (fun {α : Type u} => P) fun {β : Type v} => Q] [hP : GroundedPred fun {α : Type u} => P] {M : Matroid α} {f : α → β} {x : α} (hx : P M x) (hf : Set.InjOn f M.E) : Q (M.map f hf) (f x)

theorem Matroid.InvariantFun.map_set_image_iff {α : Type u} {β : Type v} {P : {α : Type u} → Matroid α → Set α → Prop} {Q : {β : Type v} → Matroid β → Set β → Prop} [h : InvariantFun (fun {α : Type u} => P) fun {β : Type v} => Q] {M : Matroid α} {f : α → β} {X : Set α} (hX : X ⊆ M.E) (hf : Set.InjOn f M.E) : Q (M.map f hf) (f '' X) ↔ P M X

theorem Matroid.InvariantFun.map_set_iff_exists {α : Type u} {β : Type v} {P : {α : Type u} → Matroid α → Set α → Prop} {Q : {β : Type v} → Matroid β → Set β → Prop} [h : InvariantFun (fun {α : Type u} => P) fun {β : Type v} => Q] [hP : GroundedPred fun {α : Type u} => P] [hQ : GroundedPred fun {α : Type v} => Q] {M : Matroid α} {f : α → β} {X : Set β} (hf : Set.InjOn f M.E) : Q (M.map f hf) X ↔ ∃ (X₀ : Set α), P M X₀ ∧ X = f '' X₀

theorem Matroid.InvariantFun.mapEquiv_set_iff {α : Type u} {β : Type v} {P : {α : Type u} → Matroid α → Set α → Prop} {Q : {β : Type v} → Matroid β → Set β → Prop} [h : InvariantFun (fun {α : Type u} => P) fun {β : Type v} => Q] [hP : GroundedPred fun {α : Type u} => P] [hQ : GroundedPred fun {α : Type v} => Q] {M : Matroid α} {f : α ≃ β} {X : Set β} : Q (M.mapEquiv f) X ↔ P M (⇑f ⁻¹' X)

theorem Matroid.InvariantFun.and {γ₁ : Type u → Sort u_1} {δ₁ : Type v → Sort u_4} [S₁ : Matroid.SupportClass γ₁] [T₁ : Matroid.SupportClass δ₁] [C₁ : Matroid.TransferClass γ₁ δ₁] (P P' : {α : Type u} → Matroid α → γ₁ α → Prop) (Q Q' : {β : Type v} → Matroid β → δ₁ β → Prop) [h : InvariantFun (fun {α : Type u} => P) fun {β : Type v} => Q] [h' : InvariantFun (fun {α : Type u} => P') fun {β : Type v} => Q'] : InvariantFun (fun {α : Type u} (M : Matroid α) (X : γ₁ α) => P M X ∧ P' M X) fun {β : Type v} (M : Matroid β) (X : δ₁ β) => Q M X ∧ Q' M X

theorem Matroid.InvariantFun.andSupported {γ₁ : Type u → Sort u_1} {δ₁ : Type v → Sort u_4} [S₁ : Matroid.SupportClass γ₁] [T₁ : Matroid.SupportClass δ₁] [C₁ : Matroid.TransferClass γ₁ δ₁] (P : {α : Type u} → Matroid α → γ₁ α → Prop) (Q : {β : Type v} → Matroid β → δ₁ β → Prop) [h : InvariantFun (fun {α : Type u} => P) fun {β : Type v} => Q] : InvariantFun (fun {α : Type u} (M : Matroid α) (X : γ₁ α) => P M X ∧ SupportClass.supported M X) fun {β : Type v} (M : Matroid β) (X : δ₁ β) => Q M X ∧ SupportClass.supported M X

theorem Matroid.InvariantFun.notAndSupported {γ₁ : Type u → Sort u_1} {δ₁ : Type v → Sort u_4} [S₁ : Matroid.SupportClass γ₁] [T₁ : Matroid.SupportClass δ₁] [C₁ : Matroid.TransferClass γ₁ δ₁] (P : {α : Type u} → Matroid α → γ₁ α → Prop) (Q : {β : Type v} → Matroid β → δ₁ β → Prop) [h : InvariantFun (fun {α : Type u} => P) fun {β : Type v} => Q] : InvariantFun (fun {α : Type u} (M : Matroid α) (X : γ₁ α) => ¬P M X ∧ SupportClass.supported M X) fun {β : Type v} (M : Matroid β) (X : δ₁ β) => ¬Q M X ∧ SupportClass.supported M X

theorem Matroid.InvariantFun.minimal (P : {α : Type u_9} → Matroid α → Set α → Prop) (Q : {β : Type u_10} → Matroid β → Set β → Prop) [h : InvariantFun (fun {α : Type u_9} => P) fun {β : Type u_10} => Q] [hP : GroundedPred fun {α : Type u_9} => P] : InvariantFun (fun {α : Type u_9} (M : Matroid α) (X : Set α) => Minimal (P M) X) fun {β : Type u_10} (N : Matroid β) {Y : Set β} => Minimal (Q N) Y

theorem Matroid.InvariantFun.maximal (P : {α : Type u_9} → Matroid α → Set α → Prop) (Q : {β : Type u_10} → Matroid β → Set β → Prop) [h : InvariantFun (fun {α : Type u_9} => P) fun {β : Type u_10} => Q] [hP : GroundedPred fun {α : Type u_9} => P] [hQ : GroundedPred fun {α : Type u_10} => Q] : InvariantFun (fun {α : Type u_9} (M : Matroid α) (X : Set α) => Maximal (P M) X) fun {β : Type u_10} (N : Matroid β) {Y : Set β} => Maximal (Q N) Y

instance Matroid.InvariantFun.instIndep : InvariantFun (fun {α : Type u_9} => Indep) fun {β : Type u_10} => Indep

instance Matroid.InvariantFun.instCoindep : InvariantFun (fun {α : Type u_9} => Coindep) fun {β : Type u_10} => Coindep

instance Matroid.InvariantFun.instDep : InvariantFun (fun {α : Type u_9} => Dep) fun {β : Type u_10} => Dep

instance Matroid.InvariantFun.instBase : InvariantFun (fun {α : Type u_9} => IsBase) fun {β : Type u_10} => IsBase

instance Matroid.InvariantFun.instCodep : InvariantFun (fun {α : Type u_9} => Codep) fun {β : Type u_10} => Codep

instance Matroid.InvariantFun.instSpanning : InvariantFun (fun {α : Type u_9} => Spanning) fun {β : Type u_10} => Spanning

instance Matroid.InvariantFun.instNonspanning : InvariantFun (fun {α : Type u_9} => Nonspanning) fun {β : Type u_10} => Nonspanning

instance Matroid.InvariantFun.instIsBasis : InvariantFun₂ (fun {α : Type u_9} => IsBasis) fun {β : Type u_10} => IsBasis

instance Matroid.InvariantFun.instClosure : InvariantFun (fun {α : Type u_9} => closure) fun {β : Type u_10} => closure

instance Matroid.Invariant.instFinite : Invariant (fun {α : Type u_1} => Matroid.Finite) fun {β : Type u_2} => Matroid.Finite

instance Matroid.Invariant.instNonempty : Invariant (fun {α : Type u_1} => Matroid.Nonempty) fun {β : Type u_2} => Matroid.Nonempty