ofHom_id — Mathlib

English

The morphism corresponding to the identity map id_X is the identity on TopCat.of X.

Русский

Морфизм, соответствующий тождественному отображению id_X, является тождественным морфизмом на TopCat.of X.

LaTeX

$$$\\mathrm{ofHom}(\\mathrm{ContinuousMap.id}\,X) = \\mathbf{1}_{\\mathrm{TopCat.of}(X)}$$$

Lean4

@[simp]
theorem ofHom_id {X : Type u} [TopologicalSpace X] : ofHom (ContinuousMap.id X) = 𝟙 (of X) :=
  rfl

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