instCoframe

Mathlib.Order.Sublocale

URI: https://scilib.ai/kg/mathlib#Sublocale.instCoframe

English

Sublocale X carries a coframe structure, obtained from the minimal axioms and the nucleus-isomorphism framework.

Русский

У сублокал X имеется кофрейм-структура, полученная из минимальных аксиом и рамки изоморфизма нуклеуса.

LaTeX

$$Sublocale(X) is a Coframe$$

Lean4

instance instCoframe : Order.Coframe (Sublocale X) :=
  .ofMinimalAxioms instCoframeMinimalAxioms

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

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

Разделы

Аффилиация

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