Theorems · Theorem · combinatorics

Matroid.map_closure_eq

∀ {α : Type u_2} {β : Type u_3} (M : Matroid α) (f : α → β) (hf : Set.InjOn f M.E) (X : Set β),
  (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)

Defined in

Mathlib.Combinatorics.Matroid.Closure

Cited by

2 results in Mathlib

Foundations

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