proposition: Lemma cantor_like_finite_prod (T : nat -> topologicalType) : (forall n, finite_set [set: pointed_discrete_topology (T n)]) -> (forall n, (exists xy : T n * T n, xy.1 != xy.2)) -> cantor_like (tree_of T).
proof: Proof. move=> finiteT twoElems; split. - exact/(@perfect_diagonal (pointed_discrete_topology \o T))/twoElems. - have := tychonoff (fun n => finite_compact (finiteT n)). set A := (X in compact X -> _). suff : A = [set: tree_of (fun x : nat => T x)] by move=> ->. by rewrite eqEsubset. - apply: (@hausdorff_product _ (pointed_discrete_topology \o T)) => n. by apply: discrete_hausdorff; exact: discrete_pointed. - apply: zero_dimension_prod => ?; apply: discrete_zero_dimension. exact: discrete_pointed. 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)