Syntax question about universal quantification ∀

Stream: new members

[Ender Doe]

Hi, I am going through chapter 4 in the documentation. I have a question about ∀. Is there a nice syntactic way to put a condition on a forall? For example I am going through the exercises where you define prime numbers. What I came up with was this :
def prime (n : ℕ) : Prop :=(n > 1) ∧ (∀ k : ℕ, (k = 1) ∨ ¬(divides n k)).
It seems like the ∨ part at the end is somewhat burdensome for describing a constraint. Some of the later exercises such as the Goldbach weak Conjecture were even hairier when using ∨ as a constraint mechanism.

[Yury G. Kudryashov]

all k, divides n k -> ...

[Marc Huisinga]

you can do the following:
first, transform to the variant you probably intended (you're missing the k = n case and the order in divides is mixed up)

def prime (n : ℕ) : Prop := (n > 1) ∧ (∀ k : ℕ, (k = 1) ∨ (k = n) ∨ ¬(divides k n))

then, use implication instead of or (as described by yury).

def prime (n : ℕ) : Prop := (n > 1) ∧ (∀ k : ℕ, divides k n → (k = 1) ∨ (k = n))

then, using the notation described in TPIL, you can do the following:

def prime (n : ℕ) : Prop := (n > 1) ∧ (∀ k ∣ n, (k = 1) ∨ (k = n))

[Ender Doe]

Ahh I see thank you very much.

[Kevin Buzzard]

And remember that that's \| not |