isBase_of_forall_insert — Mathlib

English

If B is independent and no element outside B can be added without breaking independence, then B is a base.

Русский

Если B независима и ни один элемент вне B не может быть добавлен, не нарушив независимость, то B является базой.

LaTeX

$$M.Indep(B) ∧ ∀ e ∈ M.E \\ B, ¬ M.Indep(B ∪ {e}) ⇒ M.IsBase(B)$$

Lean4

theorem isBase_of_forall_insert (hB : M.Indep B) (hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)) : M.IsBase B :=
  by
  refine by_contra fun hnb ↦ ?_
  obtain ⟨B', hB'⟩ := M.exists_isBase
  obtain ⟨e, he, h⟩ := hB.exists_insert_of_not_isBase hnb hB'
  exact hBmax e ⟨hB'.subset_ground he.1, he.2⟩ h

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