equal
deleted
inserted
replaced
488 |
488 |
489 lemma convex_approx: "approx_chain convex_approx" |
489 lemma convex_approx: "approx_chain convex_approx" |
490 using convex_map_ID finite_deflation_convex_map |
490 using convex_map_ID finite_deflation_convex_map |
491 unfolding convex_approx_def by (rule approx_chain_lemma1) |
491 unfolding convex_approx_def by (rule approx_chain_lemma1) |
492 |
492 |
493 definition convex_defl :: "defl \<rightarrow> defl" |
493 definition convex_defl :: "udom defl \<rightarrow> udom defl" |
494 where "convex_defl = defl_fun1 convex_approx convex_map" |
494 where "convex_defl = defl_fun1 convex_approx convex_map" |
495 |
495 |
496 lemma cast_convex_defl: |
496 lemma cast_convex_defl: |
497 "cast\<cdot>(convex_defl\<cdot>A) = |
497 "cast\<cdot>(convex_defl\<cdot>A) = |
498 udom_emb convex_approx oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj convex_approx" |
498 udom_emb convex_approx oo convex_map\<cdot>(cast\<cdot>A) oo udom_prj convex_approx" |