equal
deleted
inserted
replaced
50 lemma chain_subset_extension_on_Union: |
50 lemma chain_subset_extension_on_Union: |
51 assumes "chain\<^sub>\<subseteq> R" and "\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p" |
51 assumes "chain\<^sub>\<subseteq> R" and "\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p" |
52 shows "extension_on (Field (\<Union>R)) (\<Union>R) p" |
52 shows "extension_on (Field (\<Union>R)) (\<Union>R) p" |
53 using assms |
53 using assms |
54 by (simp add: chain_subset_def extension_on_def) |
54 by (simp add: chain_subset_def extension_on_def) |
55 (metis (no_types) mono_Field set_mp) |
55 (metis (no_types) mono_Field subsetD) |
56 |
56 |
57 lemma downset_on_empty [simp]: "downset_on {} p" |
57 lemma downset_on_empty [simp]: "downset_on {} p" |
58 by (auto simp: downset_on_def) |
58 by (auto simp: downset_on_def) |
59 |
59 |
60 lemma extension_on_empty [simp]: "extension_on {} p q" |
60 lemma extension_on_empty [simp]: "extension_on {} p q" |