coe_of

Mathlib.Topology.Order.Category.AlexDisc

URI: https://scilib.ai/kg/mathlib#AlexDisc.coe_of

English

The carrier of AlexDisc.of α is α.

Русский

Носитель AlexDisc.of α равен α.

LaTeX

$$$\operatorname{carrier}(\mathrm{AlexDisc.of}(\alpha)) = \alpha$$$

Lean4

theorem coe_of (α : Type*) [TopologicalSpace α] [AlexandrovDiscrete α] : ↥(of α) = α :=
  rfl

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

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

Разделы

Аффилиация

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