Commit e4af8b40 authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

small refinements to partition proofs

parent 72edb20655d6
This diff is collapsed.
This diff is collapsed.
......@@ -789,6 +789,9 @@ proof -
using assms by (metis Ord_linear2 Sup_least Sup_upper eq_iff mem_Collect_eq subsetD succ_le_iff)
qed
lemma in_succ_iff: "Ord i \<Longrightarrow> j \<in> elts (ZFC_in_HOL.succ i) \<longleftrightarrow> Ord j \<and> j \<le> i"
by (metis Ord_in_Ord Ord_mem_iff_lt Ord_not_le Ord_succ succ_le_iff)
lemma zero_in_succ [simp,intro]: "Ord i \<Longrightarrow> 0 \<in> elts (succ i)"
using mem_0_Ord by auto
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment