2022-04-27 14:57
src/topology/algebra/module/weak_dual.lean
feat(measure_theory/measure/finite_measure_weak_convergence): define the topology of weak convergence of measures and prove some lemmas about it. (#9943) …
Added tendsto_iff_forall_eval_tendsto_top_dual_pairing