Stream: new members

Topic: set from type

Iocta (Aug 04 2020 at 07:52):

I have

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


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

Kenny Lau (Aug 04 2020 at 07:53):

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


Iocta (Aug 04 2020 at 07:54):

oh, that was easy :-)

Iocta (Aug 04 2020 at 08:00):

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

Kenny Lau (Aug 04 2020 at 08:02):

what do you mean?

Kenny Lau (Aug 04 2020 at 08:02):

do you have an example?

Iocta (Aug 04 2020 at 08:03):

the set of all the naturals

Iocta (Aug 04 2020 at 08:04):

or do we use types there instead

Kenny Lau (Aug 04 2020 at 08:04):

set.univ

cool

Utensil Song (Aug 08 2020 at 10:27):

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

Anne Baanen (Aug 08 2020 at 10:31):

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 (Aug 08 2020 at 10:53):

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

What does univ stand for here? "universal"?

universe

Reid Barton (Aug 08 2020 at 11:32):

Or universal set perhaps

Utensil Song (Aug 08 2020 at 12:37):

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

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

Logan Murphy (Aug 08 2020 at 13:35):

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 (Aug 08 2020 at 13:47):

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 (Aug 08 2020 at 13:50):

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

Alex J. Best (Aug 08 2020 at 17:18):

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 (Aug 14 2020 at 13:00):

@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 (Aug 14 2020 at 13:33):

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 (Aug 14 2020 at 14:00):

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 (Aug 14 2020 at 14:01):

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

Last updated: May 13 2021 at 23:16 UTC