toContPerfPair_apply

Mathlib.Topology.Algebra.Module.PerfectPairing

URI: https://scilib.ai/kg/mathlib#LinearMap.toContPerfPair_apply

English

The application of the cont-perf pair matches the original linear map evaluation.

Русский

Применение пары согласуется с обычной оценкой линейного отображения.

LaTeX

$$$p.toContPerfPair(x,y) = p(x,y).$$$

Lean4

@[simp]
theorem toContPerfPair_apply (x : M) (y : N) : p.toContPerfPair x y = p x y :=
  rfl

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

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

Разделы

Аффилиация

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