English
Let f: L1 → L2 be a Lie algebra homomorphism and h1, h2, h3 be data that witness the nested construction. Then the Lie algebra hom constructed by repeatedly bundling f with h1, h2, h3 is identical to f.
Русский
Пусть f: L1 → L2 – гомоморфизм Ли, а судьбы h1, h2, h3 служат свидетельствами вложенной конструкции. Тогда гомоморфизм Ли, полученный после последовательного объединения f с h1, h2, h3, равен f.
LaTeX
$$$ (\langle\langle\langle f, h_1\rangle, h_2\rangle, h_3\rangle : L_1 \to_{\mathsf{Lie}} L_2) = f $$$
Lean4
@[simp]
theorem mk_coe (f : L₁ →ₗ⁅R⁆ L₂) (h₁ h₂ h₃) : (⟨⟨⟨f, h₁⟩, h₂⟩, h₃⟩ : L₁ →ₗ⁅R⁆ L₂) = f :=
by
ext
rfl
