instPreorder

Mathlib.Topology.Specialization

URI: https://scilib.ai/kg/mathlib#Specialization.instPreorder

English

The specialization relation on α defines a preorder on the points of α.

Русский

Отношение специализации на α задаёт структуру предпорядка на точках α.

LaTeX

$$$\text{Preorder}(\operatorname{Specialization}(\alpha))$$$

Lean4

instance instPreorder : Preorder (Specialization α) :=
  specializationPreorder α

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

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

Разделы

Аффилиация

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