const

Mathlib.LinearAlgebra.AffineSpace.AffineMap

URI: https://scilib.ai/kg/mathlib#AffineMap.const

← MathLib Explorer

English

For the constructor mk' with data f, f', p, h, coercing to a function yields f.

Русский

Для конструктора mk' с данными f, f', p, h, сведение к функции даёт f.

LaTeX

$$coe (mk' f f' p h) = f$$

Lean4

/-- The constant function as an `AffineMap`. -/
def const (p : P2) : P1 →ᵃ[k] P2 where
  toFun := Function.const P1 p
  linear := 0
  map_vadd' _
    _ :=
    letI : AddAction V2 P2 := inferInstance
    by simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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