help proving properties about subsets of N

Stream: maths

[Michael Nestor]

hey, I am trying to set up the following proof about primitive sets:

import data.nat.basic
import data.nat.factors

def is_primitive (A : set ℕ) := ∀ a ∈ A, ∀ b ∈ A, a % b > 0

variable P : set ℕ = {p | nat.prime p}

lemma is_primitive P :=
  begin
    sorry,
  end

but I am getting invalid binder declaration, delimiter/bracket expected (i.e., '(', '{', '[', '{{') after is_primitive P... what am I doing wrong here?:thinking:

[Yaël Dillies]

import data.nat.basic
import data.nat.factors

def is_primitive (A : set ℕ) := ∀ a ∈ A, ∀ b ∈ A, a % b > 0

def P : set ℕ := {p | nat.prime p}

lemma is_primitive_P : is_primitive P :=
  begin
    sorry,
  end

[Yaël Dillies]

variable is to declare local variables, not to define "global variables" (which I guess is how you were thinking of it)

[Michael Nestor]

ahh ok I should have remembered propositions<=>types! :smile: but, I still get the aforementioned error after stating the lemma

[Yaël Dillies]

Whoops, sorry, fixed

[Yaël Dillies]

You had forgotten to name the lemma and to add a colon before the lemma statement

[Michael Nestor]

got it! thank you

[Eric Wieser]

Isn't the only set satisfying your is_primitive the empty set?

[Eric Wieser]

Consider a = b

[Yaël Dillies]

Indeed. Here's a better definition:

def is_primitive (s : set ℕ) : Prop := s.pairwise $ λ a b, ¬ a ∣ b