English
If ground sets are equal and every base of the first matroid is independent in the second, and every base of the second is independent in the first, then the two matroids are equal.
Русский
Если основания матроидов совпадают по множеству оснований и пересечения, то равны матроиды.
LaTeX
$$Eq M₁.E M₂.E ∧ (∀ ⦃B⦄, M₁.IsBase B → M₂.Indep B) ∧ (∀ ⦃B⦄, M₂.IsBase B → M₁.Indep B) ⇒ M₁ = M₂$$
Lean4
/-- If every base of `M₁` is independent in `M₂` and vice versa, then `M₁ = M₂`. -/
theorem ext_isBase_indep {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (hM₁ : ∀ ⦃B⦄, M₁.IsBase B → M₂.Indep B)
(hM₂ : ∀ ⦃B⦄, M₂.IsBase B → M₁.Indep B) : M₁ = M₂ :=
by
refine ext_indep hE fun I hIE ↦ ⟨fun hI ↦ ?_, fun hI ↦ ?_⟩
· obtain ⟨B, hB, hIB⟩ := hI.exists_isBase_superset
exact (hM₁ hB).subset hIB
obtain ⟨B, hB, hIB⟩ := hI.exists_isBase_superset
exact (hM₂ hB).subset hIB
