linearIndepOn_extend — Mathlib

English

If hs is LIOn on v for s and s ⊆ t, then hs.extend hst is LIOn on v.

Русский

Если hs линейно независимо на v для s и s ⊆ t, тогда расширение hs.extend hst линейно независимо.

LaTeX

$$$$LinearIndepOn\ K\ v\ (hs.extend hst).$$$$

Lean4

theorem linearIndepOn_extend (hs : LinearIndepOn K v s) (hst : s ⊆ t) : LinearIndepOn K v (hs.extend hst) :=
  let ⟨_hbt, _hsb, _htb, hli⟩ := Classical.choose_spec (exists_linearIndepOn_extension hs hst)
  hli

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