mem_span_iff_id — Mathlib

English

Let h be LinearIndepOn K id s. Then a ∈ span_K s iff LinearIndepOn K id (insert a s) → 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 \left(a \in \operatorname{span}_K s \iff \bigl( \text{LinearIndepOn}_K(\mathrm{id},\operatorname{insert} a\,s) \rightarrow a \in s \bigr)\right)$$$

Lean4

theorem mem_span_iff_id {s : Set V} {a : V} (h : LinearIndepOn K id s) :
    a ∈ Submodule.span K s ↔ (LinearIndepOn K id (insert a s) → a ∈ s) := by simpa using h.mem_span_iff (a := a)

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