proposition: Lemma cantor_space_compact : compact [set: cantor_space].
proof: Proof. have := @tychonoff _ (fun _ : nat => _) _ (fun=> discrete_bool_compact). by congr (compact _); rewrite eqEsubset. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum interval rat) mathcomp(finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) reals signed topology HB(structures)