notMem_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 \notin \operatorname{span}_K s \iff \bigl( \text{LinearIndepOn}_K(\mathrm{id},\operatorname{insert} a\,s) \land a \notin s \bigr)\right)$$$

Lean4

theorem notMem_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 rw [h.mem_span_iff_id, _root_.not_imp]

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