English
A stronger version: two matroids with same ground set are equal if no circuit of one is independent in the other, and vice versa.
Русский
Улучшенная версия: матроиды на одинаковом основанном множестве равны, если ни одна окружность одного не независима в другом, и наоборот.
LaTeX
$$$\\forall {\\alpha} {M_1 M_2 : Matroid \\alpha}, M_1.E = M_2.E \\to (\\forall C, M_1.IsCircuit C \\to \\neg M_2.Indep C) \\to (\\forall C, M_2.IsCircuit C \\to \\neg M_1.Indep C) \\to M_1 = M_2$$$
Lean4
/-- 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. -/
theorem ext_isCircuit_not_indep {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (h₁ : ∀ C, M₁.IsCircuit C → ¬M₂.Indep C)
(h₂ : ∀ C, M₂.IsCircuit C → ¬M₁.Indep C) : M₁ = M₂ :=
by
refine ext_isCircuit hE fun C hCE ↦ ⟨fun hC ↦ ?_, fun hC ↦ ?_⟩
· obtain ⟨C', hC'C, hC'⟩ := ((not_indep_iff (by rwa [← hE])).1 (h₁ C hC)).exists_isCircuit_subset
rwa [← hC.eq_of_not_indep_subset (h₂ C' hC') hC'C]
obtain ⟨C', hC'C, hC'⟩ := ((not_indep_iff hCE).1 (h₂ C hC)).exists_isCircuit_subset
rwa [← hC.eq_of_not_indep_subset (h₁ C' hC') hC'C]
