notMem_span_iff — Mathlib

English

Let h be LinearIndepOn K f s. Then Not (f a ∈ span_K (f '' s)) is equivalent to LinearIndepOn K f (insert a s) ∧ Not (a ∈ s).

Русский

Пусть h = LinearIndepOn K f s. Тогда не принадлежность f a порождению span_K (f '' s) эквивалентна LinearIndepOn K f (insert a s) и Not (a ∈ s).

LaTeX

$$$\neg (f a \in \operatorname{span}_K(f''s)) \iff \bigl( \text{LinearIndepOn}_K f (\operatorname{insert} a\,s) \land \neg (a \in s) \bigr)$$$

Lean4

/-- A shortcut to a convenient form for the negation in `LinearIndepOn.mem_span_iff`. -/
theorem notMem_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 rw [h.mem_span_iff, _root_.not_imp]

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