comap_id

Mathlib.Topology.DiscreteQuotient

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

English

Comap along the identity map leaves the quotient unchanged.

Русский

Комап вдоль тождественного отображения сохраняет фактор.

LaTeX

$$$ S.comap(\\mathrm{id}_X) = S $$$

Lean4

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

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

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

Разделы

Аффилиация

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