Theorems · Theorem · combinatorics

Matroid.cRk_map_image_lift

∀ {α : Type u} {β : Type v} {f : α → β} (M : Matroid α) (hf : Set.InjOn f M.E) (X : Set α),
  autoParam (X ⊆ M.E) Matroid.cRk_map_image_lift._auto_1 →
    Cardinal.lift.{u, v} ((M.map f hf).cRk (f '' X)) = Cardinal.lift.{v, u} (M.cRk X)

Defined in

Mathlib.Combinatorics.Matroid.Rank.Cardinal

Cited by

1 results in Mathlib

Foundations

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