id_union — Mathlib

English

If s and t are LI on v and their spans are disjoint, then the union s∪t is LI on v.

Русский

Если s и t линейно независимы относительно v и их линейные оболочки не пересекаются, то объединение s∪t линейно независимо относительно v.

LaTeX

$$$\\text{LinearIndepOn } R\\ v\\ s \\to \\text{LinearIndepOn } R\\ v\\ t \\to \\text{Disjoint}(\\operatorname{span}R(\\operatorname{image}v s), \\operatorname{span}R(\\operatorname{image}v t)) \\to \\text{LinearIndepOn } R\\ v (s\\cup t)$$$

Lean4

theorem id_union {s t : Set M} (hs : LinearIndepOn R id s) (ht : LinearIndepOn R id t)
    (hdj : Disjoint (span R s) (span R t)) : LinearIndepOn R id (s ∪ t) :=
  hs.union ht (by simpa)

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