Theorems · Theorem · category theory

TopCat.continuous_iff_of_isColimit

∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat}
  (c : CategoryTheory.Limits.Cocone F) (hc : CategoryTheory.Limits.IsColimit c) {X : Type u'}
  [inst_1 : TopologicalSpace X] (f : ↑c.pt → X),
  Continuous f ↔ ∀ (j : J), Continuous (f ∘ ⇑(CategoryTheory.ConcreteCategory.hom (c.ι.app j)))

Defined in

Mathlib.Topology.Category.TopCat.Limits.Basic

Cited by

0 results in Mathlib

Foundations

Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryTopologicalSpace