proposition: Lemma perfect_diagonal (K : nat -> topologicalType) : (forall i, exists (xy: K i * K i), xy.1 != xy.2) -> perfect_set [set: prod_topology K].
proof: Proof. move=> npts; split; first exact: closedT. rewrite eqEsubset; split => f // _. pose distincts (i : nat) := projT1 (sigW (npts i)). pose derange (i : nat) (z : K i) := if z == (distincts i).1 then (distincts i).2 else (distincts i).1. pose g (N i : nat) := if (i < N)%nat then f i else derange _ (f i). have gcvg : g @ \oo --> f. apply/cvg_sup => N U [V] [[W] oW <-] WfN WU. by apply: (filterS WU); rewrite nbhs_simpl /g; exists N.+1 => // i /= ->. move=> A /gcvg; rewrite nbhs_simpl; case=> N _ An. exists (g N); split => //; last by apply: An; rewrite /= ?leqnn //. apply/eqP => M; suff: g N N != f N by rewrite M; move/eqP. rewrite /g ltnn /derange eq_sym; case: (eqVneq (f N) (distincts N).1) => //. by move=> ->; have := projT2 (sigW (npts N)). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed