proposition: Lemma dfwith_continuous g (i : I) : continuous (dfwith g _ : K i -> prod_topology K).
proof: Proof. move=> z U [] P [] [] Q QfinP <- [] V JV Vpz. move/(@preimage_subset _ _ (dfwith g i))/filterS; apply. apply: (@filterS _ _ _ ((dfwith g i) @^-1` V)); first by exists V. have [L Lsub /[dup] VL <-] := QfinP _ JV; rewrite preimage_bigcap. apply: filter_bigI => /= M /[dup] LM /Lsub /set_mem [] w _ [+] + /[dup] + <-. have [->|wnx] := eqVneq w i => N oN NM. apply: (@filterS _ _ _ N); first by move=> ? ?; rewrite /= dfwithin. apply: open_nbhs_nbhs; split => //; move: Vpz. by rewrite -VL => /(_ _ LM); rewrite -NM /= dfwithin. apply: nearW => y /=; move: Vpz. by rewrite -VL => /(_ _ LM); rewrite -NM /= ? dfwithout // eq_sym. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed