mem_of_insert_indep — Mathlib

English

If I is a Basis' I X and e ∈ X and I ∪ {e} is independent, then e ∈ I.

Русский

Если I — Basis' I X и e ∈ X и I ∪ {e} независима, тогда e ∈ I.

LaTeX

$$$ (hI : M.IsBasis' I X) \land e \in X \land M.Indep (I \cup \{e\}) \Rightarrow e \in I $$$

Lean4

theorem mem_of_insert_indep (hI : M.IsBasis' I X) (he : e ∈ X) (hIe : M.Indep (insert e I)) : e ∈ I :=
  hI.isBasis_inter_ground.mem_of_insert_indep ⟨he, hIe.subset_ground (mem_insert _ _)⟩ hIe

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