English
For a diagram J → LightProfinite, the limit cone 'pt' of the composed diagram with lightProfiniteToCompHaus is a totally disconnected space.
Русский
Для диаграммы J → LightProfinite предел-куб 'pt' композиции с lightProfiniteToCompHaus есть пространство, полностью разобщённое.
LaTeX
$$$\operatorname{TotallyDisconnectedSpace}( (\operatorname{CompHaus.limitCone}(F \circ \text{lightProfiniteToCompHaus})).pt.\toTop )$$$
Lean4
instance {J : Type v} [SmallCategory J] (F : J ⥤ LightProfinite.{max u v}) :
TotallyDisconnectedSpace (CompHaus.limitCone.{v, u} (F ⋙ lightProfiniteToCompHaus)).pt.toTop :=
by
change TotallyDisconnectedSpace ({u : ∀ j : J, F.obj j | _} : Type _)
exact Subtype.totallyDisconnectedSpace
