Define filter comap

[mkerjean]

Redefine fmap to f @F = f^-1 ( f^-1 F)

Define comap as comap as f @^-1 F = f^-1 (f F)

And generalize the following lemma:

https://github.com/mkerjean/analysis/blob/3837896c7793d0981ffd64ad87bb01bcc9db0f35/theories/normedtype_theory/normed_module.v#L325

Global Instance ent_xsection_filter {R : realFieldType} (U : normedZmodType R) x
  : Filter [set P | exists2 A : set (pseudoMetric_normed U *
                                     pseudoMetric_normed U),
           ent A & xsection A x `<=` P].
Proof.
apply: Build_Filter => /=.
- by exists setT => //; exact: (@entourageT (pseudoMetric_normed U)).
- move=> A B/= [A' [r/= r0 ballA'] A'A] [B' [d/= d0 ballB'] B'B].
  exists (A' `&` B'); last by rewrite xsectionI; exact: setISS.
  rewrite entourageE /entourage_.
  exists (Num.min r d); first by rewrite /= lt_min r0.
  move=> z/= Hz; split.
  + by apply: ballA' => /=; rewrite /ball/= (lt_le_trans Hz)// ge_min lexx.
  + by apply: ballB' => /=; rewrite /ball/= (lt_le_trans Hz)// ge_min lexx orbT.
- by move=> P Q PQ [A entA AP]; exists A => //; exact: (subset_trans AP).
Qed.