ext_iff_isCircuit — Mathlib

English

Equality of matroids is equivalent to equality of ground sets and equality of all circuit collections.

Русский

Равенство матроидов эквивалентно равенству их оснований и равенству всех коллекций окружностей.

LaTeX

$$$\\forall {\\alpha} {M_1 M_2 : Matroid \\alpha}, M_1 = M_2 \\iff M_1.E = M_2.E \\land \\forall C, M_1.IsCircuit C \\iff M_2.IsCircuit C$$$

Lean4

theorem ext_iff_isCircuit {M₁ M₂ : Matroid α} : M₁ = M₂ ↔ M₁.E = M₂.E ∧ ∀ C, M₁.IsCircuit C ↔ M₂.IsCircuit C :=
  ⟨fun h ↦ by simp [h], fun h ↦ ext_isCircuit h.1 fun C hC ↦ h.2 (C := C)⟩

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