coe_mk'

Mathlib.Topology.Algebra.Module.LinearMap

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.coe_mk'

English

The underlying function of the constructed map mk(f,h) is f when viewed as a plain function M1 → M2.

Русский

Основанная функция отображения mk(f,h) равна f, если рассматривать его как обычную функцию.

LaTeX

$$$ (\mathrm{mk}\, f\, h : M_1 \to M_2) = f $$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru