coe_mk'

Mathlib.LinearAlgebra.AffineSpace.AffineMap

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

English

The coercion of mk' to a function equals the constructed function f.

Русский

Приведение mk' к функции равно конструируемой функции f.

LaTeX

$$coe_mk' f f' p h = f$$

Lean4

@[simp]
theorem coe_mk' (f : P1 → P2) (f' : V1 →ₗ[k] V2) (p h) : ⇑(mk' f f' p h) = f :=
  rfl

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

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

Разделы

Аффилиация

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