English
For X ∈ LightCondSet, the topology on X(*) is the coinduced topology with respect to the coprod map coinducingCoprod X.
Русский
Для X ∈ LightCondSet топология на X(*) есть коиндукционная топология по отображению coinducingCoprod X (коиндукцированная через копроизведение).
LaTeX
$$$\mathcal{T}_X = \operatorname{coinduced}\bigl(\operatorname{coinducingCoprod} X\bigr).$$$
Lean4
/-- 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. -/
local instance underlyingTopologicalSpace : TopologicalSpace (X.val.obj ⟨LightProfinite.of PUnit⟩) :=
TopologicalSpace.coinduced (coinducingCoprod X) inferInstance
