proposition: Lemma cvg_at_leftE (R : numFieldType) (V : normedModType R) (f : R -> V) x : cvg (f @ x^') -> lim (f @ x^') = lim (f @ at_left x).
proof: Proof. move=> cvfx; apply/Logic.eq_sym. apply: (@cvg_lim _ _ _ (at_left _)) => // A /cvfx /nbhs_ballP [_ /posnumP[e] xe_A]. exists e%:num => //= y xe_y; rewrite lt_def => /andP [xney _]. by apply: xe_A => //; rewrite eq_sym. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix interval) mathcomp(mathcomp_extra boolp classical_sets functions) reals signed topology prodnormedzmodule normedtype landau forms