set from type

Stream: new members

[Iocta]

I have

inductive thing : Type
| a : thing
| b : thing
| c : thing

How do I make the set {a, b, c}?

[Kenny Lau]

open thing
#check ({a, b, c} : set thing)

[Iocta]

oh, that was easy :-)

[Iocta]

is it possible to do it in general, such as for infinite sets?

[Kenny Lau]

what do you mean?

[Kenny Lau]

do you have an example?

[Iocta]

the set of all the naturals

[Iocta]

or do we use types there instead

[Kenny Lau]

set.univ

[Iocta]

cool

[Utensil Song]

I don't really understand docs#set.univ by looking at its doc or source.

[Anne Baanen]

Sets are represented by their characteristic predicate, so the definition of set.univ means that (x : α) ∈ set.univ iff (λ a, true) x holds, i.e. set.univ is the set of all x : α.

[Utensil Song]

Thanks, that makes sense. Should have read its implementation together with docs#set.mem 's .

What does univ stand for here? "universal"?

[Reid Barton]

universe

[Reid Barton]

Or universal set perhaps

[Utensil Song]

I've checked other concepts in docs#set, there're 3 more that I don't understand :

• docs#set_of : why is it need?
• docs#set.sUnion: any reference for the notation ⋃₀ ?
• docs#set.is_lawful_singleton> any reference for the concept of a lawful singleton ?

(I understand what they mean by the equations but don't know the references for the concepts)

[Logan Murphy]

What do you mean by reference? If you're looking for examples of e.g. sUnion, you might find Ch.4 of MiL helpful: https://leanprover-community.github.io/mathematics_in_lean/sets_functions_and_relations.html

[Utensil Song]

By references I mean references outside of Lean world and in the ordinary math world, I could not find references for them by googling.

[Utensil Song]

Thanks for the link in #mil , sUnion_eq_bUnion is helpful.

[Alex J. Best]

set_of is the constructor of sets, you could use an explicit type declaration to make a set from a function to Prop but set_of is more explicit, and the notation { | } is defined as set_of.

def l := set_of (λ t : ℕ × ℕ × ℕ × ℕ × ℕ × ℕ × ℕ, nat.even t.1)
def b : set (ℕ × ℕ × ℕ × ℕ × ℕ × ℕ × ℕ) := λ t : ℕ × ℕ × ℕ × ℕ × ℕ × ℕ × ℕ, nat.even t.1
#print l
#print b

[Utensil Song]

@Mario Carneiro Do you remember why docs#set.sUnion is in Lean and docs#set.sInter is in Mathlib? (git blame traces back to your commits in 2017: lean, mathlib )

Should it stay this way?

[Mario Carneiro]

The commit to lean is marked "response to review" and seems to be referring to https://github.com/leanprover/lean/pull/1567#discussion_r114865336 . It appears that I added sUnion and sInter in this commit, renaming Union to sUnion (and a matching Inter did not exist before that commit)

[Mario Carneiro]

The source of the asymmetry appears to be https://github.com/leanprover/lean/commit/5e8572b407d7ecb8780c7cc1f5cf80ae2c373648, which was PR'd by me, I'm not sure why. Maybe it was being used by the hash_map implementation

[Mario Carneiro]

Anyway to answer your question I don't think we need sets in lean core at all, except for set_of which has special parser support