coe_of

Mathlib.Topology.Category.FinTopCat

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

English

The underlying type of the object FinTopCat.of X is exactly X.

Русский

Базовый тип объекта FinTopCat.of X равен X.

LaTeX

$$$(\\mathrm{FinTopCat}.coe\\_of)(X) : (\\mathrm{FinTopCat}.of X) = X$$$

Lean4

@[simp]
theorem coe_of (X : Type u) [Fintype X] [TopologicalSpace X] : (of X : Type u) = X :=
  rfl

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

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

Разделы

Аффилиация

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