forgetToTop_of — Mathlib

English

The forgetful functor from AlexDisc to TopCat applied to AlexDisc.of α yields TopCat.of α.

Русский

Забывающий функтор AlexDisc → TopCat, применённый к AlexDisc.of α, даёт TopCat.of α.

LaTeX

$$$(\mathrm{forget}_2\, \mathrm{AlexDisc}\, \mathrm{TopCat}).\mathrm{obj}(\mathrm{AlexDisc.of}(\alpha)) = \mathrm{TopCat.of}(\alpha)$$$

Lean4

@[simp]
theorem forgetToTop_of (α : Type*) [TopologicalSpace α] [AlexandrovDiscrete α] :
    (forget₂ AlexDisc TopCat).obj (of α) = TopCat.of α :=
  rfl

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