instCountableClopensCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology

English

For every LightProfinite S, the set of clopen subsets of its carrier is countable.

Русский

Для любого LightProfinite S множество клиопных (одновременно открытых и замкнутых) подмножеств носителя пространства является счетным.

LaTeX

$$$\operatorname{Countable}(\mathrm{Clopens}(S)).$$$

Lean4

instance (S : LightProfinite) : Countable (Clopens S) :=
  by
  rw [TopologicalSpace.Clopens.countable_iff_secondCountable]
  infer_instance

Похожие утверждения