proposition: Lemma perfect_set2 {T} : perfect_set [set: T] <-> forall (U : set T), open U -> U !=set0 -> exists x y, [/\ U x, U y & x != y] .
proof: Proof. apply: iff_trans; first exact: perfectTP; split. move=> nx1 U oU [] x Ux; exists x. have : U <> [set x] by move=> Ux1; apply: (nx1 x); rewrite -Ux1. apply: contra_notP; move/not_existsP/contrapT=> Uyx; rewrite eqEsubset. (split => //; last by move=> ? ->); move=> y Uy; have /not_and3P := Uyx y. by case => // /negP; rewrite negbK => /eqP ->. move=> Unxy x Ox; have [] := Unxy _ Ox; first by exists x. by move=> y [] ? [->] -> /eqP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed