Theorems · Theorem · category theory

ContinuousGeneratedByCat.fromGeneratedByTopCat_map_hom_apply

∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {X_1 Y : GeneratedByTopCat X} (f : X_1 ⟶ Y)
  (a : ↑X_1.obj),
  (ContinuousGeneratedByCat.fromGeneratedByTopCat.map f).hom a = (CategoryTheory.ConcreteCategory.hom f) a

Defined in

Mathlib.Topology.Convenient.Category

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpace