duplicate documentation

[affeldt-aist]

analysis/theories/topology_theory/separation_axioms.v

Lines 41 to 55 in 069bc57

	(* perfect_set A == A is closed, and every point in A is *)
	(* a limit point of A *)
	(* ``` *)
	(* ## metrizability for uniform spaces *)
	(* ``` *)
	(* countable_uniform.type == endows a pseudoMetric on a uniform type whose *)
	(* entourage has a countable basis *)
	(* sup_pseudometric == the pseudometric induced for the supremum *)
	(* of countably many pseudoMetrics *)
	(* gauge E == for an entourage E, gauge E is a filter which *)
	(* includes `iter n split_ent E`. *)
	(* Critically, `gauge E` forms a uniform space *)
	(* with a countable uniformity. *)
	(* perfect_set A := closed A /\ limit_point A = A *)
	(* ``` *)

the documentation for perfect_set is duplicated