isEqualizer

Mathlib.Order.Category.OmegaCompletePartialOrder

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

Lean4

/-- The equalizer fork is a limit. -/
def isEqualizer {X Y : ωCPO.{v}} (f g : X ⟶ Y) : IsLimit (equalizer f g) :=
  Fork.IsLimit.mk' _ fun s =>
    ⟨{  toFun := fun x => ⟨s.ι x, by apply ContinuousHom.congr_fun s.condition⟩
        monotone' := fun _ _ h => s.ι.monotone h
        map_ωSup' := fun x => Subtype.ext (s.ι.continuous x) }, by ext; rfl, fun hm =>
      by
      ext x : 2;
      apply
        Subtype.ext
          ?_ -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): Originally `ext`

      apply ContinuousHom.congr_fun hm⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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