proposition: Lemma repr_comp_continuous (Z : topologicalType) (g : T -> Z) : continuous g -> {homo g : a b / \pi_Q a == \pi_Q b :> Q >-> a == b} -> continuous (g \o repr : Q -> Z).
proof: Proof. move=> /continuousP ctsG rgE; apply/continuousP => A oA. rewrite /open/= /quotient_open (_ : _ @^-1` _ = g @^-1` A); first exact: ctsG. have greprE x : g (repr (\pi_Q x)) = g x by apply/eqP; rewrite rgE// reprK. by rewrite eqEsubset; split => x /=; rewrite greprE. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed