mem_span_iff — Mathlib

English

Let h be LinearIndepOn K id s. Then a ∈ span_K s if and only if LinearIndepOn K id (insert a s) implies a ∈ s.

Русский

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

LaTeX

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

Lean4

theorem mem_span_iff {s : Set ι} {a : ι} {f : ι → V} (h : LinearIndepOn K f s) :
    f a ∈ Submodule.span K (f '' s) ↔ (LinearIndepOn K f (insert a s) → a ∈ s) :=
  by
  by_cases has : a ∈ s
  · exact iff_of_true (subset_span <| mem_image_of_mem f has) fun _ ↦ has
  simp [linearIndepOn_insert_iff, h, has]

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