instHasLimitWalkingParallelPairParallelPair

Mathlib.Order.Category.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#ωCPO.instHasLimitWalkingParallelPairParallelPair

English

For any pair of parallel arrows f,g: X ⇒ Y in ωCPO, there is a limit (i.e., equalizer).

Русский

Для любой пары параллельных стрелок f,g: X ⇒ Y в ωCPO существует предел (равнитель).

LaTeX

$$$\operatorname{HasLimit}(\mathrm{parallelPair}\, f\, g)$ for all f,g$$$

Lean4

instance {X Y : ωCPO.{v}} (f g : X ⟶ Y) : HasLimit (parallelPair f g) :=
  HasLimit.mk ⟨_, HasEqualizers.isEqualizer f g⟩

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

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

Разделы

Аффилиация

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