Clopen Sets

[zstone1]

Motivation for this change

Being totally disconnected is a key feature of cantor space theory. The cantor space is the unique space (up to homeomorphism) that is "metrizable + compact + perfect + totally disconnected". Turns out proving this with clopen sets is much easier than dealing with arbitrary separations.

This PR defines clopen, totally disconnected, and second-countable, and proves a handful of basics facts. The main results are

• Clopen sets form a countable basis for compact, metrizable, totally disconnected spaces (by way of second countability).
• The cantor space is totally disconnected (as a product of discrete spaces). Likewise, products of the cantor spaces are totally disconnected.

As a side note, this is also step one for proving Stone Representation Theorem. Although I'm not pursuing this angle right now.

Things done/to do

• added corresponding entries in CHANGELOG_UNRELEASED.md
  (do not edit former entries, only append new ones, be careful:
  merge and rebase have a tendency to mess up CHANGELOG_UNRELEASED.md)
• added corresponding documentation in the headers

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[affeldt-aist]

Would it be better to have a definition of second_countable made of "smaller" definitions such as:

Definition local_base (T : topologicalType) (x : T) (B : set (set T)) :=
  B `<=` nbhs x /\ (forall V, nbhs x V -> exists2 A, B A & A `<=` V).

Definition topological_base (T : topologicalType) (B : set (set T)) :=
  B `<=` open /\ forall x, exists2 C, C `<=` B & local_base x C.

Definition second_countable' (T : topologicalType) := exists2 B : set (set T),
  countable B & topological_base B.

Lemma second_countableP (T : topologicalType) :
  second_countable T <-> second_countable' T.
Proof.
split=> [[B [cB Bopen h]]|].
  exists B => //; split => // x.
  have {}h := h x.
  have @h' : forall V : {V : set T & nbhs x V}, {A : set T | [/\ B A, nbhs x A & A `<=` projT1 V]}.
    move=> [V Vx]; apply: cid.
    by move: (h V Vx) => [W [BW xW WV]]; exists W.
  exists [set V | exists W (xW : nbhs x W), sval (h' (existT _ _ xW)) = V].
    by move=> _ /= [W [xW /=]] <-; case: cid => // ? [].
  split.
    by move=> _ /= [W [xW] <-]; case: cid => ? [].
  move=> V xV; exists (projT1 (h' (existT _ _ xV))).
    by exists V, xV.
  by move=> y/=; rewrite /sval/=; case: cid => W [BW xW WV Wy]; exact: WV.
move=> [B cB [Bopen h]]; exists B; split => // x V xV.
have [C CB [Cx h']] := h x.
have [A CA AV] := h' _ xV.
by exists A; split => //; [exact: CB|exact: Cx].
Qed.

[zstone1]

Need to make things more friendly for working with subsets.

[zstone1]

I will treat all the 2nd countability stuff mentioned here in a separate diff.

In the meanwhile, stuff on clopen and connectedness is simpler, and now presented without the 2nd countability stuff in #840