English
Let K be a division ring and V a K-vector space. For any subset s of V and elements x,y ∈ V, if x belongs to the span of insert y s but not to the span of s, then y belongs to the span of insert x s.
Русский
Пусть K — деление кольцо, V — K-пространство, s ⊆ V, x,y ∈ V. Если x принадлежит порождению (insert y s), но не принадлежит порождению s, то y принадлежит порождению (insert x s).
LaTeX
$$$x \in \operatorname{span}_K(\operatorname{insert} y\,s) \Rightarrow x \notin \operatorname{span}_K(s) \Rightarrow y \in \operatorname{span}_K(\operatorname{insert} x\,s)$$$
Lean4
theorem mem_span_insert_exchange : x ∈ span K (insert y s) → x ∉ span K s → y ∈ span K (insert x s) :=
by
simp only [mem_span_insert, forall_exists_index, and_imp]
rintro a z hz rfl h
refine ⟨a⁻¹, -a⁻¹ • z, smul_mem _ _ hz, ?_⟩
have a0 : a ≠ 0 := by
rintro rfl
simp_all
match_scalars <;> simp [a0]
