proposition: Lemma pointwise_compact_cvg (F : set_system {ptws X -> Y}) (f : {ptws X -> Y}) : ProperFilter F -> (\forall W \near powerset_filter_from F, equicontinuous W id) -> {ptws, F --> f} <-> {family compact, F --> f}.
proof: Proof. move=> PF /near_powerset_filter_fromP; case. exact: equicontinuous_subset_id. move=> W; wlog Wf : f W / W f. move=> + FW /equicontinuous_closure => /(_ f (closure (W : set {ptws X -> Y}))) Q. split => Ff; last by apply: pointwise_cvg_compact_family. apply/Q => //. by rewrite closureEcvg; exists F; [|split] => // ? /= /filterS; apply. by apply: (filterS _ FW) => z Wz; apply: subset_closure. move=> FW ectsW; split=> [ptwsF|]; last exact: pointwise_cvg_compact_family. apply/fam_cvgP => K ? U /=; rewrite uniform_nbhs => [[E [eE EsubU]]]. suff : \forall g \near within W (nbhs (f : {ptws X -> Y})), forall y, K y -> E (f y, g y). rewrite near_withinE; near_simpl => N; apply: (filter_app _ _ FW). by apply: ptwsF; near=> g => ?; apply: EsubU; apply: (near N g). near (powerset_filter_from (@entourage Y)) => E'. have entE' : entourage E' by exact: (near (near_small_set _)). pose Q := fun (h : X -> Y) x => E' (f x, h x). apply: (iffLR (compact_near_coveringP K)) => // x Kx. near=> y g => /=. apply: (entourage_split (f x) eE). apply entourage_sym; apply: (near (small_ent_sub _) E') => //. exact: (near (ectsW x E' entE') y). apply: (@entourage_split _ (g x)) => //. apply: (near (small_ent_sub _) E') => //. near: g; near_simpl; apply: (@cvg_within _ (nbhs (f : {ptws X -> Y}))). exact: pointwise_cvg_entourage. apply: (near (small_ent_sub _) E') => //. apply: (near (ectsW x E' entE')) => //. exact: (near (withinT _ (nbhs_filter (f : {ptws X -> 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