insert_not_indep — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem insert_not_indep (hI : M.IsBasis' I X) (he : e ∈ X \ I) : ¬M.Indep (insert e I) := fun hi ↦
  he.2 <| insert_eq_self.1 <| Eq.symm <| hI.eq_of_subset_indep hi (subset_insert _ _) (insert_subset he.1 hI.subset)

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