[STATEMENT]
lemma cblinfun_blinfun_transfer_tendsto[cblinfun_blinfun_transfer]:
  includes lifting_syntax
  shows "(((=) ===> blinfun_cblinfun_eq) ===> blinfun_cblinfun_eq ===> (=) ===> (=)) tendsto tendsto"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((=) ===> blinfun_cblinfun_eq) ===> blinfun_cblinfun_eq ===> (=) ===> (=)) (\<longlongrightarrow>) (\<longlongrightarrow>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (((=) ===> blinfun_cblinfun_eq) ===> blinfun_cblinfun_eq ===> (=) ===> (=)) (\<longlongrightarrow>) (\<longlongrightarrow>)
[PROOF STEP]
note cblinfun_blinfun_transfer[transfer_rule]
[PROOF STATE]
proof (state)
this:
blinfun_cblinfun_eq 0 0
(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) (+) (+)
(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) (-) (-)
(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) uminus uminus
(real_complex_eq ===> blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) (*\<^sub>R) (*\<^sub>C)
(eq_onp bounded_clinear ===> blinfun_cblinfun_eq) Blinfun CBlinfun
(blinfun_cblinfun_eq ===> (=)) norm norm
(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq ===> (=)) dist dist
(blinfun_cblinfun_eq ===> blinfun_cblinfun_eq) sgn sgn
(((=) ===> blinfun_cblinfun_eq) ===> (=)) Cauchy Cauchy

goal (1 subgoal):
 1. (((=) ===> blinfun_cblinfun_eq) ===> blinfun_cblinfun_eq ===> (=) ===> (=)) (\<longlongrightarrow>) (\<longlongrightarrow>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((=) ===> blinfun_cblinfun_eq) ===> blinfun_cblinfun_eq ===> (=) ===> (=)) (\<longlongrightarrow>) (\<longlongrightarrow>)
[PROOF STEP]
unfolding tendsto_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((=) ===> blinfun_cblinfun_eq) ===> blinfun_cblinfun_eq ===> (=) ===> (=)) (\<lambda>f l F. \<forall>e>0. \<forall>\<^sub>F x in F. dist (f x) l < e) (\<lambda>f l F. \<forall>e>0. \<forall>\<^sub>F x in F. dist (f x) l < e)
[PROOF STEP]
by transfer_prover
[PROOF STATE]
proof (state)
this:
(((=) ===> blinfun_cblinfun_eq) ===> blinfun_cblinfun_eq ===> (=) ===> (=)) (\<longlongrightarrow>) (\<longlongrightarrow>)

goal:
No subgoals!
[PROOF STEP]
qed