Theorems · Theorem · category theory

LightCondSet.toTopCatMap_hom_apply

∀ {X Y : LightCondSet} (f : X ⟶ Y) (a : X.obj.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))),
  (TopCat.Hom.hom (LightCondSet.toTopCatMap f)) a =
    (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op (LightProfinite.of PUnit.{u + 1})))) a

Defined in

Mathlib.Condensed.Light.TopCatAdjunction

Cited by

0 results in Mathlib

Foundations

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