isBasis_of_forall_insert — Mathlib

English

Let M be a matroid, I ⊆ X, and suppose I is independent and every e ∈ X \\ I satisfies that I ∪ {e} is dependent. Then I is a basis of X.

Русский

Пусть M — матроид, I ⊆ X, и предположим, что I независим, а для каждого e ∈ X \\ I множество I ∪ {e} зависимо. Тогда I является базисом X.

LaTeX

$$$ (M.Indep I) \\land (I \\subseteq X) \\land \\left( \\forall e \\in X \\setminus I,\\ M.Dep(I \\cup \\{e\\}) \\right) \\Rightarrow M.IsBasis I X $$$

Lean4

theorem isBasis_of_forall_insert (hI : M.Indep I) (hIX : I ⊆ X) (he : ∀ e ∈ X \ I, M.Dep (insert e I)) :
    M.IsBasis I X :=
  (hI.isBasis_iff_forall_insert_dep hIX).mpr he

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