proposition: Lemma is_linear_fst {K : AbsRing} {U V : NormedModule K} : is_linear (fun t : U * V => fst t).
proof: Proof. split. - intros [x1 x2] [y1 y2] ; by simpl. - intros k [x1 x2] ; by simpl. - exists 1 ; split. exact Rlt_0_1. intros [x1 x2] ; simpl fst ; rewrite Rmult_1_l. eapply Rle_trans. 2: by apply norm_prod. by apply Rmax_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv