insert_dep — Mathlib

English

If B is a base and e lies in the ground set outside B, then B ∪ {e} is dependent.

Русский

Если B — база, и элемент e принадлежит ground set и не принадлежит B, тогда B ∪ {e} зависим.

LaTeX

$$M.IsBase(B) \\land e \\in M.E \\setminus B \\Rightarrow M.Dep(B \\cup \\{e\\})$$

Lean4

theorem insert_dep (hB : M.IsBase B) (h : e ∈ M.E \ B) : M.Dep (insert e B) :=
  by
  rw [← not_indep_iff (insert_subset h.1 hB.subset_ground)]
  exact h.2 ∘ (fun hi ↦ insert_eq_self.mp (hB.eq_of_subset_indep hi (subset_insert e B)).symm)

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