proposition: Lemma weak_subspace_open (A : set (weak_topology f)) : open A -> open (f @` A : set (subspace (range f))).
proof: Proof. case=> B oB <-; apply/open_subspaceP; exists B; split => //; rewrite eqEsubset. split => z [] /[swap]; first by case=> w _ <- ?; split; exists w. by case=> w _ <- [v] ? <-. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed