ext_iff_isBase — Mathlib

English

There is an equivalence between M1 = M2 and the combination of equal ground sets and identical base relations.

Русский

Существуют эквивалентности между равенством матроидов и сочетанием равного множества оснований и тождественных отношений баз.

LaTeX

$$theorem ext_isBase {M1 M2 : Matroid α} (hE : M1.E = M2.E) (h : ∀ ⦃B⦄, B ⊆ M1.E → (M1.IsBase B ↔ M2.IsBase B)) : M1 = M2$$

Lean4

theorem ext_iff_isBase {M₁ M₂ : Matroid α} : M₁ = M₂ ↔ M₁.E = M₂.E ∧ ∀ ⦃B⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B) :=
  ⟨fun h ↦ by simp [h], fun ⟨hE, h⟩ ↦ ext_isBase hE h⟩

Похожие утверждения