equal
deleted
inserted
replaced
72 qed |
72 qed |
73 |
73 |
74 subsection {* Continuity of @{const case_lift} *} |
74 subsection {* Continuity of @{const case_lift} *} |
75 |
75 |
76 lemma case_lift_eq: "case_lift \<bottom> f x = fup\<cdot>(\<Lambda> y. f (undiscr y))\<cdot>(Rep_lift x)" |
76 lemma case_lift_eq: "case_lift \<bottom> f x = fup\<cdot>(\<Lambda> y. f (undiscr y))\<cdot>(Rep_lift x)" |
77 apply (induct x, unfold lift.cases) |
77 apply (induct x, unfold lift.case) |
78 apply (simp add: Rep_lift_strict) |
78 apply (simp add: Rep_lift_strict) |
79 apply (simp add: Def_def Abs_lift_inverse) |
79 apply (simp add: Def_def Abs_lift_inverse) |
80 done |
80 done |
81 |
81 |
82 lemma cont2cont_case_lift [simp]: |
82 lemma cont2cont_case_lift [simp]: |