instSequentialSpaceCarrierObjTopCatLightCondSetToTopCat

English

For any X in LightCondSet, the carrier of the object lightCondSetToTopCat.obj X is a sequential space.

Русский

Для любого X в LightCondSet носитель объекта lightCondSetToTopCat.obj X имеет последовательную топологию.

LaTeX

$$$\operatorname{SequentialSpace}\left((\text{lightCondSetToTopCat}.obj X)\text{.carrier}\right)$$$

Lean4

instance (X : LightCondSet.{u}) : SequentialSpace (lightCondSetToTopCat.obj X) :=
  inferInstanceAs (SequentialSpace X.toTopCat)

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