exchange_isBase_of_indep' — Mathlib

English

If B is a base, e ∈ B, f ∉ B, and I is independent with insert f B \ { e }, then the resulting set is a base.

Русский

Если B база, e ∈ B, f ∉ B, и I независимо (insert f B \ { e }), тогда получившаяся множина является базой.

LaTeX

$$$ M.IsBase B \rightarrow e \in B \rightarrow f \notin B \rightarrow M.Indep (\operatorname{insert} f B \ { e }) \rightarrow M.IsBase (\operatorname{insert} f B \ { e })$$$

Lean4

theorem exchange_isBase_of_indep' (hB : M.IsBase B) (he : e ∈ B) (hf : f ∉ B) (hI : M.Indep (insert f B \ { e })) :
    M.IsBase (insert f B \ { e }) :=
  by
  have hfe : f ≠ e := ne_of_mem_of_not_mem he hf |>.symm
  rw [← insert_diff_singleton_comm hfe] at *
  exact hB.exchange_isBase_of_indep hf hI

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