mem_of_insert_indep — Mathlib

English

If B is a base and inserting e into B preserves independence, then e belongs to B.

Русский

Если B является базой и вставка элемента e в B сохраняет независимость, тогда e ∈ B.

LaTeX

$$$ M.IsBase B \rightarrow M.Indep (\text{insert } e B) \rightarrow e \in B $$$

Lean4

theorem mem_of_insert_indep (hB : M.IsBase B) (heB : M.Indep (insert e B)) : e ∈ B :=
  by_contra fun he ↦ (hB.dep_of_insert he (heB.subset_ground (mem_insert _ _))).not_indep heB

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