instTopologicalSpaceCarrierCarrier

Mathlib.Geometry.RingedSpace.PresheafedSpace

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.PresheafedSpace.instTopologicalSpaceCarrierCarrier

English

The topology on the carrier of a presheafed space is given by its carrier's structure.

Русский

Топология носителя прешефдов пространства задаётся структурой носителя.

LaTeX

$$$\text{TopSpaceCarrier}(X) = X.carrier.str$$$

Lean4

instance (X : PresheafedSpace C) : TopologicalSpace X :=
  X.carrier.str

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru