comap_id

Mathlib.Topology.LocallyConstant.Basic

URI: https://scilib.ai/kg/mathlib#LocallyConstant.comap_id

English

Pullback along the identity map is the identity on LocallyConstant(X, Z).

Русский

Тянущее вдоль тождественного отображения сохраняет идентичность для LocallyConstant(X, Z).

LaTeX

$$$ comap\\ (\\text{ContinuousMap.id } X) = id\\ (LocallyConstant\\ X\\ Z) $$$

Lean4

@[simp]
theorem comap_id : comap (@ContinuousMap.id X _) = @id (LocallyConstant X Z) :=
  rfl

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

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

Разделы

Аффилиация

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