English
Two matroids M1 and M2 are equal iff they have the same ground set and the same base predicate on all subsets.
Русский
Матроиды M1 и M2 равны тогда и только тогда, когда у них одинаковое множество оснований и одинаковая характеристика базы для всех подмножеств.
LaTeX
$$∀ {α} {M1 M2 : Matroid α}, Eq M1.E M2.E → (∀ ⦃B : Set α⦄, B ⊆ M1.E → (M1.IsBase B ↔ M2.IsBase B)) → M1 = M2$$
Lean4
theorem ext_isBase {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (h : ∀ ⦃B⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B)) :
M₁ = M₂ :=
by
have h' : ∀ B, M₁.IsBase B ↔ M₂.IsBase B := fun B ↦
⟨fun hB ↦ (h hB.subset_ground).1 hB, fun hB ↦ (h <| hB.subset_ground.trans_eq hE.symm).2 hB⟩
ext <;> simp [hE, M₁.indep_iff', M₂.indep_iff', h']
