linearIndepOn_id_insert_iff — Mathlib

English

For any a and s, LinearIndepOn K id (insert a s) is equivalent to LinearIndepOn K id s together with a ∈ span K s → a ∈ s.

Русский

Для a и s: LinearIndepOn K id (insert a s) эквивалентно LinearIndepOn K id s и условию, что если a лежит в span K s тогда a ∈ s.

LaTeX

$$$\operatorname{LinearIndepOn}_K(\mathrm{id},\operatorname{insert} a\,s) \iff \operatorname{LinearIndepOn}_K(\mathrm{id},s) \land (a \in \operatorname{span}_K s \rightarrow a \in s)$$$

Lean4

theorem linearIndepOn_id_insert_iff {a : V} {s : Set V} :
    LinearIndepOn K id (insert a s) ↔ LinearIndepOn K id s ∧ (a ∈ span K s → a ∈ s) := by
  simpa using linearIndepOn_insert_iff (a := a) (f := id)

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