Email Gateway (Aug 18 2022 at 18:02): Email Gateway (Aug 18 2022 at 18:02):From: 游珍 <yucy0405@163.com>
Dear friends,
I have a promble about verifying the next lemma.
lemma add_finite : "finite A \<and> A \<noteq> {} \<Longrightarrow> finite {(x::nat) + m |m. m \<in> A}"
Need your help! Thanks.
yucy
Email Gateway (Aug 18 2022 at 18:02):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear yucy,
perhaps you want to use finite_imageI:
lemma add_finite : "finite A \<Longrightarrow> finite {(x::nat) + m |m. m \<in> A}"
proof -
assume f: "finite A"
have id: "{x + m | m. m \<in> A} = (\<lambda>m. x + m) ` A" by auto
from finite_imageI[OF f]
show ?thesis unfolding id .
qed
Cheers,
René
Email Gateway (Aug 18 2022 at 18:02):From: Tobias Nipkow <nipkow@in.tum.de>
The trick is that {e | m. m : A} is equivalent to (%m. e) A. Now you
can use the lemma finite_imageI: finite ?F ==> finite (?h ?F)
lemma add_finite : "finite A ==> finite {(x::nat) + m |m. m : A}"
using finite_imageI[of A "%m. x+m"]
by(simp add: image_def)
Note that A ~= {} is unnecessary.
Tobias
Last updated: Apr 24 2024 at 12:33 UTC