Theorems · Definition · combinatorics

Matroid.map

{α : Type u_1} → {β : Type u_2} → (M : Matroid α) → (f : α → β) → Set.InjOn f M.E → Matroid β

Given a function f that is injective on M.E, the copy of M in β whose independent sets are the images of those in M. If β is a nonempty type, then N : Matroid β is a map of M if and only if M and N are isomorphic.

Defined in

Mathlib.Combinatorics.Matroid.Map

Cited by

32 results in Mathlib

Foundations

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