ext_closure — Mathlib

English

Let M1 and M2 be matroids on α. If for every subset X ⊆ α we have closure_{M1}(X) = closure_{M2}(X), then M1 = M2.

Русский

Пусть M1 и M2 — матроиды на α. Если для каждого подмножества X ⊆ α выполнено cl_{M1}(X) = cl_{M2}(X), то M1 = M2.

LaTeX

$$$$ \forall X \subseteq \alpha, \ \operatorname{cl}_{M_1}(X) = \operatorname{cl}_{M_2}(X) \Rightarrow M_1 = M_2. $$$$

Lean4

theorem ext_closure {M₁ M₂ : Matroid α} (h : ∀ X, M₁.closure X = M₂.closure X) : M₁ = M₂ :=
  ext_indep (by simpa using h univ) (fun _ _ ↦ by simp_rw [indep_iff_forall_closure_diff_ne, h])

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