coe_mk — Mathlib

English

The underlying function of the nested LieHom built from f and h1,h2,h3 is exactly f.

Русский

Вложенная конструция LieHom из 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) : L_1 \to L_2) = f $$$

Lean4

@[simp]
theorem coe_mk (f : L₁ → L₂) (h₁ h₂ h₃) : ((⟨⟨⟨f, h₁⟩, h₂⟩, h₃⟩ : L₁ →ₗ⁅R⁆ L₂) : L₁ → L₂) = f :=
  rfl

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