proposition: Lemma sup_ent_inv A : sup_ent A -> sup_ent (A^-1)%classic.
proof: Proof. move=> [B [F ? FB] BA]; exists (B^-1)%classic; last by move=> ?; exact: BA. have inv : forall ie : IEnt, ent_of ((projT1 ie).1, ((projT1 ie).2)^-1)%classic. by IEntP=> ?? /entourage_inv ??; exact/asboolP. exists [fset (fun x => @exist (I * set (T * T)) _ _ (inv x)) w | w in F]%fset. by move=> ? /imfsetP; IEntP => ???? ->; exact: in_setT. rewrite -FB eqEsubset; split; case=> x y + ie. by move=> /(_ (exist ent_of _ (inv ie))) + ?; apply; apply/imfsetP; exists ie. by move=> + /imfsetP [v vW ->]; exact. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed