proposition: Lemma compact_equicontinuous (W : set {family compact, X -> Y}) : (forall f, W f -> continuous f) -> compact (W : set {family compact, X -> Y}) -> equicontinuous W id.
proof: Proof. move=> ctsW cptW x E entE. have [//|U UWx [cptU clU]] := @lcptX x; rewrite withinET in UWx. near (powerset_filter_from (@entourage Y)) => E'. have entE' : entourage E' by exact: (near (near_small_set _)). pose Q := fun (y : X) (f : {family compact, X -> Y}) => E' (f x, f y). apply: (iffLR (compact_near_coveringP W)) => // f Wf; near=> g y => /=. apply: (entourage_split (f x) entE). apply/entourage_sym; apply: (near (small_ent_sub _) E') => //. exact: (near (fam_nbhs _ entE' (@compact_set1 _ x)) g). apply: (entourage_split (f y) (entourage_split_ent entE)). apply: (near (small_ent_sub _) E') => //. by near: y; apply: ((@ctsW f Wf x) (to_set _ _)); exact: nbhs_entourage. apply: (near (small_ent_sub _) E') => //. by apply: (near (fam_nbhs _ entE' cptU) g) => //; exact: (near UWx y). Unshelve. all: 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