coe_mk — Mathlib

English

For any σ12-semilinear map f and a proof h that f is continuous, the constructed object mk(f,h) represents the same semilinear map f; i.e., its underlying map is f.

Русский

Для любого σ12-семилинейного отображения f и доказательства h непрерывности f сконструированный объект mk(f,h) представляет то же самое отображение f; то есть его основанная функция равна f.

LaTeX

$$$\bigl(\mathrm{mk}\; f\; h \;:\; M_1 \toSL[\sigma_{12}] M_2\bigr) = f$$$

Lean4

theorem coe_mk (f : M₁ →ₛₗ[σ₁₂] M₂) (h) : (mk f h : M₁ →ₛₗ[σ₁₂] M₂) = f :=
  rfl

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