id — Mathlib · SciLib

English

The identity map on α, viewed as a cocompact map, is a cocompact map from α to α.

Русский

Идентичное отображение на α, рассматриваемое как коккомпактная карта, есть коккомпактная карта α → α.

LaTeX

$$$\\text{CocompactMap}.id(\\alpha) : CocompactMap(\\alpha, \\alpha)$$$

Lean4

/-- The identity as a cocompact continuous map. -/
protected def id : CocompactMap α α :=
  ⟨ContinuousMap.id _, tendsto_id⟩

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