proposition: Theorem Ascoli (W : set {family compact, X -> Y}) : locally_compact [set: X] -> pointwise_precompact W id /\ equicontinuous W id <-> (forall f, W f -> continuous f) /\ precompact (W : set {family compact, X -> Y}).
proof: Proof. move=> lcpt; split => [[Wid ectsW]|[fWf]pcptW]. split=> [?|]; first exact: equicontinuous_continuous. exact: pointwise_precompact_equicontinuous. split; last exact: precompact_equicontinuous. exact: precompact_pointwise_precompact. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed