Theorems · Theorem · combinatorics
Matroid.cRk_comap_lift
∀ {α : Type u} {β : Type v} (M : Matroid β) (f : α → β) (X : Set α),
Cardinal.lift.{v, u} ((M.comap f).cRk X) = Cardinal.lift.{u, v} (M.cRk (f '' X))- Cited by
- 1 results in Mathlib
- Foundations
- Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites34
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Set.Elemproof · cited by 7,166
- Set.imagestatement and proof · cited by 5,609
- Set.preimageproof · cited by 4,946
- Set.rangeproof · cited by 4,705
- LE.le.transproof · cited by 3,151
- Cardinalstatement and proof · cited by 2,598
- iSupproof · cited by 2,415
- Matroidstatement and proof · cited by 1,258
- Cardinal.mkproof · cited by 942
- Cardinal.liftstatement and proof · cited by 583
- Set.InjOnproof · cited by 543
Cited by1
Results whose statement or proof uses this declaration.
- Matroid.cRk_comapproof · cited by 0