equal
deleted
inserted
replaced
984 using ISO by auto |
984 using ISO by auto |
985 qed |
985 qed |
986 |
986 |
987 lemma iso_Field: |
987 lemma iso_Field: |
988 "iso r r' f \<Longrightarrow> f ` (Field r) = Field r'" |
988 "iso r r' f \<Longrightarrow> f ` (Field r) = Field r'" |
989 using assms by (auto simp add: iso_def bij_betw_def) |
989 by (auto simp add: iso_def bij_betw_def) |
990 |
990 |
991 lemma iso_iff: |
991 lemma iso_iff: |
992 assumes "Well_order r" |
992 assumes "Well_order r" |
993 shows "iso r r' f = (embed r r' f \<and> f ` (Field r) = Field r')" |
993 shows "iso r r' f = (embed r r' f \<and> f ` (Field r) = Field r')" |
994 proof |
994 proof |