Theorems · Theorem · combinatorics

Matroid.map_isBasis_iff

∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} {I X : Set α} (f : α → β) (hf : Set.InjOn f M.E),
  I ⊆ M.E → X ⊆ M.E → ((M.map f hf).IsBasis (f '' I) (f '' X) ↔ M.IsBasis I X)

Defined in

Mathlib.Combinatorics.Matroid.Map

Cited by

1 results in Mathlib

Foundations

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