coe_const'

Mathlib.Topology.CompactOpen

URI: https://scilib.ai/kg/mathlib#ContinuousMap.coe_const'

English

The coercion between const' and the standard constant map coincides: (const' : Y → C(X,Y)) = const X.

Русский

Сопоставление между const' и стандартной константой совпадает: (const' : Y → C(X,Y)) = константа X.

LaTeX

$$$(\text{const'} : Y \to C(X,Y)) = \text{const } X$$$

Lean4

@[simp]
theorem coe_const' : (const' : Y → C(X, Y)) = const X :=
  rfl

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

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

Разделы

Аффилиация

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