Theorems · Theorem · combinatorics

Matroid.IsBasis.map

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

Defined in

Mathlib.Combinatorics.Matroid.Map

Cited by

6 results in Mathlib

Foundations

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