Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Set Comprehention {5n. n€N} without existence-...

Email Gateway (Aug 22 2022 at 13:32):

From: Jonathan Woodgate via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hello,
is there any alternative way of writing {5n.n€N} other than {k. \ex n. k = 5n}..such as using with "forAll" operator or so (thus avoiding the existence-quantor?)
Thank you!

Email Gateway (Aug 22 2022 at 13:32):

From: Lars Hupel <hupel@in.tum.de>
Hi Jonathan,

try this:

{5 * n | n. n ∈ ℕ}

Cheers
Lars

Email Gateway (Aug 22 2022 at 13:32):

From: David Cock <david.cock@inf.ethz.ch>
{n. n mod 5 = 0}

Email Gateway (Aug 22 2022 at 13:32):

From: Jonathan Woodgate via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Thank you!

Mario Carneiro <di.gama@gmail.com> schrieb am 13:20 Montag, 6.Juni 2016:

Yes, that is the ideal (5), which is the smallest ideal containing 5. I
don't know the Isabelle notation, but that would be something like

{n. forall i in Ideals(N), 5 in i => n in i}

where i in Ideals(N) if ax+b in i whenever a,b in i and x in N.

Mario

Email Gateway (Aug 22 2022 at 13:32):

From: Jonathan Woodgate via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Thanx!

Lars Hupel <hupel@in.tum.de> schrieb am 13:12 Montag, 6.Juni 2016:

Hi Jonathan,

try this:

{5 * n | n. n ∈ ℕ}

Cheers
Lars

Last updated: Apr 30 2024 at 01:06 UTC