Theorems · Theorem · combinatorics

Matroid.comap_isBasis_iff

∀ {α : Type u_1} {β : Type u_2} {f : α → β} {N : Matroid β} {I X : Set α},
  (N.comap f).IsBasis I X ↔ N.IsBasis (f '' I) (f '' X) ∧ Set.InjOn f I ∧ I ⊆ X

Defined in

Mathlib.Combinatorics.Matroid.Map

Cited by

2 results in Mathlib

Foundations

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