Theorems · Definition · category theory

LightCondSet.underlyingTopologicalSpace

(X : LightCondSet) → TopologicalSpace (X.obj.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))

Let X be a light condensed set. We define a topology on X(*) as the quotient topology of all the maps from light profinite sets S to X(*), corresponding to elements of X(S). In other words, the topology coinduced by the map LightCondSet.coinducingCoprod above.

Defined in

Mathlib.Condensed.Light.TopCatAdjunction

Cited by

2 results in Mathlib

Foundations

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