English
Two matroids with the same ground set are equal if they have the same circuit structure on all subsets.
Русский
Два матроида на одной опорной (ground) множестве равны, если совпадает набор окружностей на всех подмножеств.
LaTeX
$$$\\forall {\\alpha} {M_1 M_2 : Matroid \\alpha}, M_1.E = M_2.E \\to (\\forall C, C ⊆ M_1.E \\to (M_1.IsCircuit C \\leftrightarrow M_2.IsCircuit C)) \\to M_1 = M_2$$$
Lean4
theorem ext_isCircuit {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (h : ∀ ⦃C⦄, C ⊆ M₁.E → (M₁.IsCircuit C ↔ M₂.IsCircuit C)) :
M₁ = M₂ :=
by
have h' {C} : M₁.IsCircuit C ↔ M₂.IsCircuit C :=
(em (C ⊆ M₁.E)).elim (h (C := C))
(fun hC ↦
iff_of_false (mt IsCircuit.subset_ground hC) (mt IsCircuit.subset_ground fun hss ↦ hC (hss.trans_eq hE.symm)))
refine ext_indep hE fun I hI ↦ ?_
simp_rw [indep_iff_forall_subset_not_isCircuit hI, h', indep_iff_forall_subset_not_isCircuit (hI.trans_eq hE)]
