instTopologicalSpaceCarrier — Mathlib

English

On objects of the finite-type category FintypeCat, the scoped topological space structure is discrete.

Русский

На объектах категории конечных типов FintypeCat задана дискретная топология.

LaTeX

$$$\\text{scoped instance } (X \\in \\mathrm{FintypeCat}) : \\mathrm{TopologicalSpace}(X) = \\bot$$$

Lean4

/-- Scoped topological space instance on objects of the category of finite types, assigning
the discrete topology. -/
scoped instance (X : FintypeCat) : TopologicalSpace X :=
  ⊥

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