src/HOL/Library/Zorn.thy
changeset 52821 05eb2d77b195
parent 52199 d25fc4c0ff62
child 53374 a14d2a854c02
equal deleted inserted replaced
52820:cb53b44b958c 52821:05eb2d77b195
   754 
   754 
   755 lemma chain_subset_extension_on_Union:
   755 lemma chain_subset_extension_on_Union:
   756   assumes "chain\<^sub>\<subseteq> R" and "\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p"
   756   assumes "chain\<^sub>\<subseteq> R" and "\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p"
   757   shows "extension_on (Field (\<Union>R)) (\<Union>R) p"
   757   shows "extension_on (Field (\<Union>R)) (\<Union>R) p"
   758   using assms
   758   using assms
   759   by (simp add: chain_subset_def extension_on_def)
   759   by (simp add: chain_subset_def extension_on_def) (metis mono_Field set_mp)
   760      (metis Field_def mono_Field set_mp)
       
   761 
   760 
   762 lemma downset_on_empty [simp]: "downset_on {} p"
   761 lemma downset_on_empty [simp]: "downset_on {} p"
   763   by (auto simp: downset_on_def)
   762   by (auto simp: downset_on_def)
   764 
   763 
   765 lemma extension_on_empty [simp]: "extension_on {} p q"
   764 lemma extension_on_empty [simp]: "extension_on {} p q"