Infinite-Dimensional Linear Algebra and Solvability of Partial Differential Equations

by TODOR D. TODOROV

We prove some elementary versions of the statement that the standard basis of ℝ³ is linearly independent.

theorem indep₀ (c₀ : ℝ) (c₁ : ℝ) (c₂ : ℝ) : c₀ • ![1, 0, 0] + c₁ • ![0, 1, 0] + c₂ • ![0, 0, 1] = ![c₀, c₁, c₂]

theorem indep₁ (c₀ : ℝ) (c₁ : ℝ) (c₂ : ℝ) (h : c₀ • ![1, 0, 0] + c₁ • ![0, 1, 0] + c₂ • ![0, 0, 1] = 0) : c₀ = 0 ∧ c₁ = 0 ∧ c₂ = 0

theorem indep₂ (c : Fin 3 → ℝ) (h : c 0 • ![1, 0, 0] + c 1 • ![0, 1, 0] + c 2 • ![0, 0, 1] = 0) : c = 0

theorem indep₃ (c : Fin 3 → ℝ) (h : c 0 • Function.update 0 0 1 + c 1 • Function.update 0 1 1 + c 2 • Function.update 0 2 1 = 0) : c = 0