Theorems · Definition · combinatorics

Matroid.comapOn

{α : Type u_1} → {β : Type u_2} → Matroid β → Set α → (α → β) → Matroid α

The pullback of a matroid on β by a function f : α → β to a matroid on α, restricted to a ground set E. The matroids M.comapOn f E and M ↾ (f '' E) have isomorphic simplifications; elements with the same nonloop image are parallel.

Defined in

Mathlib.Combinatorics.Matroid.Map

Cited by

8 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound