English
Two matroids with identical ground set and identical independence relation on all subets containing elements of the ground set are equal.
Русский
Два матроида с одинаковым базовым множеством и одинаковыми отношениями независимости на всех подмножеств из базового множества равны между собой.
LaTeX
$$M₁.E = M₂.E ∧ ∀ I ⊆ M₁.E, M₁.Indep(I) ↔ M₂.Indep(I) ⇒ M₁ = M₂$$
Lean4
@[ext]
theorem ext_indep {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (h : ∀ ⦃I⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)) : M₁ = M₂ :=
have h' : M₁.Indep = M₂.Indep := by
ext I
by_cases hI : I ⊆ M₁.E
· rwa [h]
exact iff_of_false (fun hi ↦ hI hi.subset_ground) (fun hi ↦ hI (hi.subset_ground.trans_eq hE.symm))
ext_isBase hE (fun B _ ↦ by simp_rw [isBase_iff_maximal_indep, h'])
