linearIndepOn_id_insert — Mathlib

English

For id-family, a ∉ span_K s is equivalent to independence on insert a s together with a ∉ s.

Русский

Для последовательности id не принадлежит span_K s тогда независимость на insert a s вместе с a ∉ s.

LaTeX

$$$\text{LinearIndepOn}_K(\text{id},s) \Rightarrow \Bigl( a \notin \operatorname{span}_K(s) \Rightarrow \text{LinearIndepOn}_K(\text{id},\operatorname{insert} a\,s) \land a \notin s \Bigr)$$$

Lean4

theorem linearIndepOn_id_insert (hxs : x ∉ s) :
    LinearIndepOn K id (insert x s) ↔ LinearIndepOn K id s ∧ x ∉ Submodule.span K s :=
  (linearIndepOn_insert (f := id) hxs).trans <| by simp

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