proposition: Lemma fam_compact_nbhs {U : topologicalType} {V : uniformType} (A : set U) (O : set V) (f : {family compact, U -> V}) : open O -> f @` A `<=` O -> compact A -> continuous f -> nbhs (f : {family compact, U -> V}) [set g | forall y, A y -> O (g y)].
proof: Proof. move=> oO fAO /[dup] cA /compact_near_coveringP/near_covering_withinP cfA ctsf. near=> z => /=; (suff: A `<=` [set y | O (z y)] by exact); near: z. apply: cfA => x Ax; have : O (f x) by exact: fAO. move: (oO); rewrite openE /= => /[apply] /[dup] /ctsf Ofx /=. rewrite /interior -nbhs_entourageE => -[E entE EfO]. exists (f @^-1` to_set (split_ent E) (f x), [set g | forall w, A w -> split_ent E (f w, g w)]). split => //=; last exact: fam_nbhs. by apply: ctsf; rewrite /= -nbhs_entourageE; exists (split_ent E). case=> y g [/= Efxy] AEg Ay; apply: EfO; apply: subset_split_ent => //. by exists (f y) => //=; exact: AEg. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed