proposition: Lemma filter_inv {T : Type} (F : set (set (T * T))) : Filter F -> Filter [set (V^-1)%classic | V in F].
proof: Proof. move=> FF; split => /=. - by exists [set: T * T] => //; exact: filterT. - by move=> P Q [R FR <-] [S FS <-]; exists (R `&` S) => //; exact: filterI. - move=> P Q PQ [R FR RP]; exists Q^-1%classic => //; first last. by rewrite eqEsubset; split; case. by apply: filterS FR; case=> ? ? /= ?; apply: PQ; rewrite -RP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed