English
For any light profinite object S and predicate p on S, the subtype {s | p(s)} carries a totally disconnected space structure and a second countable topology.
Русский
Для любого светлого профинитного объекта S и предиката p на S подтип {s | p(s)} несет топологию полностью раздельного пространства и вторую счетную топологию.
LaTeX
$$$\forall S\,(p:S\to\mathrm{Prop}),\ \mathrm{HasProp}\bigl(\lambda X.\operatorname{TotallyDisconnectedSpace}X.carrier \land \operatorname{SecondCountableTopology}X.carrier\bigr)\bigl(\operatorname{subtype}\,p\bigr)$$$
Lean4
/-- The functor from sets to light condensed sets given by locally constant maps into the set. -/
abbrev functor : Type u ⥤ LightCondSet.{u} :=
CompHausLike.LocallyConstant.functor.{u, u} (P := fun X ↦ TotallyDisconnectedSpace X ∧ SecondCountableTopology X)
(hs := fun _ _ _ ↦ (LightProfinite.effectiveEpi_iff_surjective _).mp)
