building a set from a sequence

Stream: new members

[Connor Gordon]

Suppose I have a sequence A i indexed by some set I. How would I build the set {A i : i ∈ I} in Lean?

[Eric Rodriguez]

docs#set.image

[Junyan Xu]

maybe docs#set.range instead

[Connor Gordon]

Alright, that makes sense, but I realized now that I said it was indexed by a set but in fact it is indexed by a type (i.e. I have a function f : ℕ → 'a and would like to construct the set {f n : n ∈ ℕ}. Using set.image doesn't seem to work because ℕ is a type, rather than a set. Any idea how to work with that?

[Connor Gordon]

Never mind, set.range got it! Thanks for the help!

[Kyle Miller]

By the way, for your original formulation you can write {(A i) : (i ∈ I)}. (This should work, but I didn't test it.)

[Kyle Miller]

The second would be {(f n) : (n : ℕ)}

[Kyle Miller]

It might be better to use docs#set.range though to get access to more lemmas.

[Eric Rodriguez]

you don't need it in this case as Junyan shows, but set.univ is the set of all elements of a type

[Eric Rodriguez]

Kyle, I can't seem to get that cool-looking notation to work.

[Kyle Miller]

These seem to work for me:

example : set ℕ := {(2 * n) | (n : ℕ)}

def f (n : ℕ) : ℕ := 2 * n
example : set ℕ := {(f n) | (n : ℕ)}

example (s : set ℕ) := {(2 * n) | (n ∈ s)}

[Matt Diamond]

@Kyle Miller your first example had : in the middle instead of |... I think that may have been why it wasn't working for Eric