proposition: Lemma linear_cont (l : U -> V) (x : U) : is_linear l -> continuous l x.
proof: Proof. intros Hl. apply filterlim_locally_ball_norm => eps. apply locally_le_locally_norm. case: (linear_norm _ Hl) => M Hn. assert (0 < eps / M). apply Rdiv_lt_0_compat. apply cond_pos. apply Hn. exists (mkposreal _ H) => y Hy. rewrite /ball_norm -linear_minus //. eapply Rle_lt_trans. by apply Hn. evar_last. apply Rmult_lt_compat_l with (2 := Hy). apply Hn. simpl. field. apply Rgt_not_eq, Hn. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv