instPreorder

Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

URI: https://scilib.ai/kg/mathlib#SSet.N.instPreorder

English

There is a natural Preorder on X.N induced by the map to SSet.N.

Русский

Для X.N задан естественный порядок по отображению в SSet.N.

LaTeX

$$$\text{instance } : Preorder X.N \;=\; Preorder.lift( toS )$$$

Lean4

instance : Preorder X.N :=
  Preorder.lift toS

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

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

Разделы

Аффилиация

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