linearIndepOn_insert_iff — Mathlib

English

Let h be LinearIndepOn K f s. Then f a ∈ span_K(f s) if and only if, whenever LinearIndepOn K f (insert a s) holds, we have a ∈ s.

Русский

Пусть h = LinearIndepOn K f s. Тогда f a ∈ span_K(f s) тогда и только тогда, когда если LinearIndepOn K f (insert a s), то a ∈ s.

LaTeX

$$$\text{LinearIndepOn}_K f s \Rightarrow\left( f a \in \operatorname{span}_K(f '' s) \iff \bigl( \text{LinearIndepOn}_K f (\operatorname{insert} a\,s) \rightarrow a \in s \bigr) \right)$$$

Lean4

theorem linearIndepOn_insert_iff {s : Set ι} {a : ι} {f : ι → V} :
    LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ (f a ∈ span K (f '' s) → a ∈ s) :=
  by
  by_cases has : a ∈ s
  · simp [insert_eq_of_mem has, has]
  simp [linearIndepOn_insert has, has]

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