instFrameElemRangeCoe

Mathlib.Order.Nucleus

URI: https://scilib.ai/kg/mathlib#Nucleus.instFrameElemRangeCoe

English

The range of a nucleus carries a frame structure, i.e., is a frame with the inherited order.

Русский

Диапазон нуклеуса имеет структуру рамы, т.е. является рамой с унаследованным порядком.

LaTeX

$$$\\text{Frame}(\\operatorname{range}(n))$$$

Lean4

instance : Frame (range n) :=
  .ofMinimalAxioms range.instFrameMinimalAxioms

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

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

Разделы

Аффилиация

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