Theorems · Theorem · combinatorics

Matroid.ext_isCircuit_not_indep

∀ {α : Type u_1} {M₁ M₂ : Matroid α},
  M₁.E = M₂.E → (∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C) → (∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C) → M₁ = M₂

A stronger version of Matroid.ext_isCircuit: two matroids on the same ground set are equal if no circuit of one is independent in the other.

Defined in

Mathlib.Combinatorics.Matroid.Circuit

Cited by

0 results in Mathlib

Foundations

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