coe_mkNormedAddGroupHom — Mathlib

English

For f : V1 → V2 and data h1,h2,h3 defining a NormedAddGroupHom, the underlying function of the constructed morphism equals f.

Русский

Для f : V1 → V2 и данных h1,h2,h3, задающих NormedAddGroupHom, базовая функция сконструированного морфизма равна f.

LaTeX

$$$\\forall x:\\ V_1,\\ (\\langle f,h_1,h_2,h_3\\rangle)(x)=f(x)$$$

Lean4

@[simp]
theorem coe_mkNormedAddGroupHom (f : V₁ →+ V₂) (C) (hC) : ⇑(f.mkNormedAddGroupHom C hC) = f :=
  rfl

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