equal
deleted
inserted
replaced
2384 shows "polyhedron (h ` S) \<longleftrightarrow> polyhedron S" |
2384 shows "polyhedron (h ` S) \<longleftrightarrow> polyhedron S" |
2385 proof - |
2385 proof - |
2386 have *: "{f. P f} = (image h) ` {f. P (h ` f)}" for P |
2386 have *: "{f. P f} = (image h) ` {f. P (h ` f)}" for P |
2387 apply safe |
2387 apply safe |
2388 apply (rule_tac x="inv h ` x" in image_eqI) |
2388 apply (rule_tac x="inv h ` x" in image_eqI) |
2389 apply (auto simp: \<open>bij h\<close> bij_is_surj image_surj_f_inv_f) |
2389 apply (auto simp: \<open>bij h\<close> bij_is_surj image_f_inv_f) |
2390 done |
2390 done |
2391 have "inj h" using bij_is_inj assms by blast |
2391 have "inj h" using bij_is_inj assms by blast |
2392 then have injim: "inj_on (op ` h) A" for A |
2392 then have injim: "inj_on (op ` h) A" for A |
2393 by (simp add: inj_on_def inj_image_eq_iff) |
2393 by (simp add: inj_on_def inj_image_eq_iff) |
2394 show ?thesis |
2394 show ?thesis |