coe_const

Mathlib.LinearAlgebra.AffineSpace.AffineMap

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

English

The function equalities hold when projecting from mk' back to function

Русский

Неравенства функций сохраняются при проекции из mk' обратно в функцию

LaTeX

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

Lean4

@[simp]
theorem coe_const (p : P2) : ⇑(const k P1 p) = Function.const P1 p :=
  rfl

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

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

Разделы

Аффилиация

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