ι

Mathlib.Topology.Category.CompHausLike.Limits

URI: https://scilib.ai/kg/mathlib#CompHausLike.finiteCoproduct.ι

Lean4

/-- The inclusion of one of the factors into the explicit finite coproduct.
-/
def ι (a : α) : X a ⟶ finiteCoproduct X :=
  ofHom _
    { toFun := fun x ↦ ⟨a, x⟩
      continuous_toFun := continuous_sigmaMk (σ := fun a ↦ X a) }

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

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

Разделы

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

Аффилиация

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