Theorems · Definition · combinatorics

Matroid.restrictSubtype

{α : Type u_1} → Matroid α → (X : Set α) → Matroid ↑X

Given M : Matroid α and X : Set α, the restriction of M to X, viewed as a matroid on type X with ground set univ. Always isomorphic to M ↾ X. If X = M.E, then isomorphic to M.

Defined in

Mathlib.Combinatorics.Matroid.Map

Cited by

16 results in Mathlib

Foundations

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