instHasExplicitPullbacksTrue

Mathlib.Topology.Category.CompHaus.Limits

URI: https://scilib.ai/kg/mathlib#CompHaus.instHasExplicitPullbacksTrue

English

In the category CompHaus, the functor constant at True has explicit pullbacks.

Русский

В категории CompHaus существуют явные pullbacks для константного диаграммного значения True.

LaTeX

$$$\operatorname{HasExplicitPullbacks}(\text{const}_{\text{True}})$$$

Lean4

instance : HasExplicitPullbacks (fun _ ↦ True) where hasProp _ _ := inferInstance

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

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

Разделы

Аффилиация

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