[STATEMENT]
lemma transfer_sup_continuous[transfer_rule]:
  "(rel_fun (rel_fun (=) pcr_ennreal) (=)) sup_continuous sup_continuous"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fun (rel_fun (=) pcr_ennreal) (=) sup_continuous sup_continuous
[PROOF STEP]
proof (safe intro!: rel_funI dest!: rel_fun_eq_pcr_ennreal[THEN iffD1])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. sup_continuous (enn2ereal \<circ> y) \<Longrightarrow> sup_continuous y
 2. \<And>x y. sup_continuous y \<Longrightarrow> sup_continuous (enn2ereal \<circ> y)
[PROOF STEP]
show "sup_continuous (enn2ereal \<circ> f) \<Longrightarrow> sup_continuous f" for f :: "'a \<Rightarrow> _"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_continuous (enn2ereal \<circ> f) \<Longrightarrow> sup_continuous f
[PROOF STEP]
using sup_continuous_e2ennreal[of "enn2ereal \<circ> f"]
[PROOF STATE]
proof (prove)
using this:
sup_continuous (enn2ereal \<circ> f) \<Longrightarrow> sup_continuous (\<lambda>x. e2ennreal ((enn2ereal \<circ> f) x))

goal (1 subgoal):
 1. sup_continuous (enn2ereal \<circ> f) \<Longrightarrow> sup_continuous f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sup_continuous (enn2ereal \<circ> ?f) \<Longrightarrow> sup_continuous ?f

goal (1 subgoal):
 1. \<And>x y. sup_continuous y \<Longrightarrow> sup_continuous (enn2ereal \<circ> y)
[PROOF STEP]
show "sup_continuous f \<Longrightarrow> sup_continuous (enn2ereal \<circ> f)" for f :: "'a \<Rightarrow> _"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_continuous f \<Longrightarrow> sup_continuous (enn2ereal \<circ> f)
[PROOF STEP]
using sup_continuous_enn2ereal[of f]
[PROOF STATE]
proof (prove)
using this:
sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. enn2ereal (f x))

goal (1 subgoal):
 1. sup_continuous f \<Longrightarrow> sup_continuous (enn2ereal \<circ> f)
[PROOF STEP]
by (simp add: comp_def)
[PROOF STATE]
proof (state)
this:
sup_continuous ?f \<Longrightarrow> sup_continuous (enn2ereal \<circ> ?f)

goal:
No subgoals!
[PROOF STEP]
qed