proposition: Lemma compact_open_fam_compactP (f : U -> V) (F : set_system (U -> V)) : continuous f -> Filter F -> {compact-open, F --> f} <-> {family compact, F --> f}.
proof: Proof. move=> ctsf FF; split; first last. move=> cptF; apply/compact_open_cvgP => K O cptK oO fKO. apply: cptF; have := fam_compact_nbhs oO fKO cptK ctsf; apply: filter_app. by near=> g => /= gKO ? [z Kx <-]; exact: gKO. move/compact_open_cvgP=> cptOF; apply/cvg_sup => -[K cptK R]. case=> D [[E oE <-] Ekf] /filterS; apply. move: oE; rewrite openE => /(_ _ Ekf); case => A [J entJ] EKR KfE. near=> z; apply/KfE/EKR => -[u Kp]; rewrite /= /set_val /= /eqincl /incl. (have Ku : K u by rewrite inE in Kp); move: u Ku {D Kp}; near: z. move/compact_near_coveringP/near_covering_withinP : (cptK); apply. move=> u Ku; near (powerset_filter_from (@entourage V)) => E'. have entE' : entourage E' by exact: (near (near_small_set _)). pose C := f @^-1` to_set E' (f u). pose B := \bigcup_(z in K `&` closure C) interior (to_set E' (f z)). have oB : open B by apply: bigcup_open => ? ?; exact: open_interior. have fKB : f @` (K `&` closure C) `<=` B. move=> _ [z KCz <-]; exists z => //; rewrite /interior. by rewrite -nbhs_entourageE; exists E'. have cptKC : compact (K `&` closure C). by apply: compact_closedI => //; exact: closed_closure. have := cptOF (K `&` closure C) B cptKC oB fKB. exists (C, [set g | [set g x | x in K `&` closure C] `<=` B]). split; last exact: cptOF. by apply: (ctsf) => //; rewrite /filter_of -nbhs_entourageE; exists E'. case=> z h /= [Cz KB Kz]. case: (KB (h z)); first by exists z; split => //; exact: subset_closure. move=> w [Kw Cw /interior_subset Jfwhz]; apply: subset_split_ent => //. exists (f w); last apply: (near (small_ent_sub _) E') => //. apply: subset_split_ent => //; exists (f u). by apply/entourage_sym; apply: (near (small_ent_sub _) E'). have [] := Cw (f@^-1` (to_set E' (f w))). by apply: ctsf; rewrite /= -nbhs_entourageE; exists E'. move=> r [Cr /= Ewr]; apply: subset_split_ent => //; exists (f r). exact: (near (small_ent_sub _) E'). by apply/entourage_sym; apply: (near (small_ent_sub _) E'). 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