id_insert — Mathlib

English

If hs asserts linear independence of id on a set s, and x is not in the span of s, then inserting x preserves linear independence of id on the enlarged set.

Русский

Если hs утверждает линейную независимость id на множестве s, и x не лежит в span(s), то добавление x сохраняет независимость.

LaTeX

$$hs : LinearIndepOn K id s, hx : x ∉ span K s ⟹ LinearIndepOn K id (insert x s)$$

Lean4

protected theorem id_insert (hs : LinearIndepOn K id s) (hx : x ∉ span K s) : LinearIndepOn K id (insert x s) :=
  hs.insert ((image_id s).symm ▸ hx)

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