piFanIsLimit

Mathlib.Topology.Category.TopCat.Limits.Products

URI: https://scilib.ai/kg/mathlib#TopCat.piFanIsLimit

Lean4

/-- The constructed fan is indeed a limit -/
def piFanIsLimit {ι : Type v} (α : ι → TopCat.{max v u}) : IsLimit (piFan α)
    where
  lift
    S :=
    ofHom
      { toFun := fun s i => S.π.app ⟨i⟩ s
        continuous_toFun := continuous_pi (fun i => (S.π.app ⟨i⟩).hom.2) }
  uniq := by
    intro S m h
    ext x
    funext i
    simp [ContinuousMap.coe_mk, ← h ⟨i⟩]
  fac _ _ := rfl

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

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

Разделы

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

Аффилиация

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