vec3_eq — Mathlib

English

Componentwise equality of 3-element vectors: if a0=b0, a1=b1, a2=b2 then [a0,a1,a2] = [b0,b1,b2].

Русский

По компонентам равенство вектора длины 3: если a0=b0, a1=b1, a2=b2, то [a0,a1,a2] = [b0,b1,b2].

LaTeX

$$$[a_0,a_1,a_2] = [b_0,b_1,b_2] \quad\text{если} \; a_0=b_0, a_1=b_1, a_2=b_2$$$

Lean4

theorem vec3_eq {a₀ a₁ a₂ b₀ b₁ b₂ : α} (h₀ : a₀ = b₀) (h₁ : a₁ = b₁) (h₂ : a₂ = b₂) : ![a₀, a₁, a₂] = ![b₀, b₁, b₂] :=
  by simp [h₀, h₁, h₂]

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