English
For x, y, z ∈ M, membership in span of {x, y, z} is equivalent to the existence of coefficients a, b, c ∈ R such that w = a x + b y + c z.
Русский
Пусть x, y, z ∈ M. Принадлежность к линейной оболочке множества {x, y, z} эквивалентна существованию коэффициентов a, b, c ∈ R таких, что w = a x + b y + c z.
LaTeX
$$$ w \in \operatorname{span}_R\left(\{x, y, z\}\right) \Longleftrightarrow \exists a,b,c \in R, a \cdot x + b \cdot y + c \cdot z = w $$$
Lean4
theorem mem_span_triple {w x y z : M} : w ∈ span R ({ x, y, z } : Set M) ↔ ∃ a b c : R, a • x + b • y + c • z = w :=
by
rw [mem_span_insert]
simp_rw [mem_span_pair]
refine exists_congr fun a ↦ ⟨?_, ?_⟩
· rintro ⟨u, ⟨b, c, rfl⟩, rfl⟩
exact ⟨b, c, by rw [add_assoc]⟩
· rintro ⟨b, c, rfl⟩
exact ⟨b • y + c • z, ⟨b, c, rfl⟩, by rw [add_assoc]⟩
