proposition: Lemma mx_ent_nbhsE : nbhs = nbhs_ mx_ent.
proof: Proof. rewrite predeq2E => M A; split. move=> [B]; rewrite -nbhs_entourageE => M_B sBA. set sB := fun i j => [set C | entourage C /\ to_set C (M i j) `<=` B i j]. have {}M_B : forall i j, sB i j !=set0 by move=> ??; apply/exists2P/M_B. exists [set MN : 'M[T]_(m, n) * 'M[T]_(m, n) | forall i j, get (sB i j) (MN.1 i j, MN.2 i j)]. by exists (fun i j => get (sB i j)) => // i j; have /getPex [] := M_B i j. move=> N CMN; apply/sBA => i j; have /getPex [_] := M_B i j; apply. exact/CMN. move=> [B [C entC sCB] sBA]; exists (fun i j => to_set (C i j) (M i j)). by rewrite -nbhs_entourageE => i j; exists (C i j). by move=> N CMN; apply/sBA/sCB. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed