proposition: Lemma cvgerNyP u : ((u x)%:E @[x --> F] --> -oo) <-> (u @ F --> -oo%R).
proof: Proof. split=> [/cvgeNyPler|/cvgrNyPler] Foo. by apply/cvgrNyPler => A Ar; near do rewrite -lee_fin; apply: Foo. by apply/cvgeNyPler => A Ar; near do rewrite lee_fin; apply: Foo. Unshelve. all: end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule