instOf

Mathlib.Topology.Compactness.DeltaGeneratedSpace

URI: https://scilib.ai/kg/mathlib#DeltaGeneratedSpace.instOf

English

The type ΔGeneratedSpace.of X carries a delta-generated space structure.

Русский

Тип ΔGeneratedSpace.of X имеет структуру дельта-генерируемого пространства.

LaTeX

$$$$\DeltaGeneratedSpace(\mathrm{of}\,X)$$$$

Lean4

instance : DeltaGeneratedSpace (of X) :=
  deltaGeneratedSpace_deltaGenerated

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

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

Разделы

Аффилиация

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