ofHom — Mathlib

English

Typecheck a ContinuousMap as a morphism in TopCat. That is, a continuous map f: X → Y corresponds to a morphism TopCat.of X ⟶ TopCat.of Y via ofHom f.

Русский

Пусть f: X → Y — непрерывное отображение. Оно даёт морфизм TopCat.of X ⟶ TopCat.of Y через ofHom f.

LaTeX

$$$\\mathrm{ofHom}: C(X, Y) \\to \\mathrm{Hom}_{\\mathrm{TopCat}}(\\mathrm{of}(X), \\mathrm{of}(Y))$$$

Lean4

/-- Typecheck a `ContinuousMap` as a morphism in `TopCat`. -/
abbrev ofHom {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : of X ⟶ of Y :=
  ConcreteCategory.ofHom (C := TopCat) f

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