ext_iff_indep — Mathlib

English

Two matroids are equal if and only if they have the same ground set and the independence relation coincides on all subsets of that ground set.

Русский

Два матроидa равны тогда и только тогда, когда они имеют одинаковое основание и совпадают отношения независимости на всех подмножеств этого основания.

LaTeX

$$M₁ = M₂ ↔ (M₁.E = M₂.E) ∧ ∀ ⦃I⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)$$

Lean4

theorem ext_iff_indep {M₁ M₂ : Matroid α} : M₁ = M₂ ↔ (M₁.E = M₂.E) ∧ ∀ ⦃I⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I) :=
  ⟨fun h ↦ by (subst h; simp), fun h ↦ ext_indep h.1 h.2⟩

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