isBasis_insert_iff — Mathlib

English

For any independent I and any e, I is a basis of I ∪ {e} if and only if either I ∪ {e} is dependent or e ∈ I.

Русский

Для любого независимого I и элемента e набор I является базисом I ∪ {e} тогда и только тогда, когда либо I ∪ {e} зависим, либо e ∈ I.

LaTeX

$$$ M.IsBasis I (I \\cup \\{e\\}) \\iff M.Dep(I \\cup \\{e\\}) \\lor e \\in I $$$

Lean4

theorem isBasis_insert_iff (hI : M.Indep I) : M.IsBasis I (insert e I) ↔ M.Dep (insert e I) ∨ e ∈ I :=
  by
  simp_rw [hI.isBasis_iff_forall_insert_dep (subset_insert _ _), dep_iff, insert_subset_iff,
    and_iff_left hI.subset_ground, mem_diff, mem_insert_iff, or_and_right, and_not_self, or_false, and_imp, forall_eq]
  tauto

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