Theorems · Definition · combinatorics

Matroid.IsStrictMinor

{α : Type u_1} → Matroid α → Matroid α → Prop

N is a strict minor of M if N is a minor of M and N ≠ M. Equivalently, N is obtained from M by deleting/contracting subsets of the ground set that are not both empty.

Defined in

Mathlib.Combinatorics.Matroid.Minor.Order

Cited by

12 results in Mathlib

Foundations

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