Ω

Mathlib.CategoryTheory.Topos.Classifier

URI: https://scilib.ai/kg/mathlib#CategoryTheory.HasClassifier.Ω

Lean4

/-- Notation for the `Ω` in an arbitrary choice of a subobject classifier -/
abbrev Ω : C :=
  HasClassifier.exists_classifier.some.Ω

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

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

Разделы

Аффилиация

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