proposition: Lemma discrete_pointed (T : pointedType) : discrete_space (pointed_discrete_topology T).
proof: Proof. apply/funext => /= x; apply/funext => A; apply/propext; split. - by move=> [E hE EA] x0 ->{x0}; apply: EA => /=; apply: hE => /=; exists x. - move=> h; exists [set x | x.1 = x.2]; first by move=> -[a b] [t _] [<- <-]. by move=> y /= xy; exact: h. 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)