## Stream: new members

### Topic: set notation

#### Patrick Thomas (Oct 10 2020 at 19:00):

Could someone point me to or tell me what the underlying definition of {} is? For instance, the singleton set {x}. I haven't been able to find it in mathlib.

#### Patrick Thomas (Oct 10 2020 at 19:05):

Nevermind, I guess VIsual Code says it is singleton.

#### Patrick Thomas (Oct 10 2020 at 19:08):

Hmm, but then set.singleton uses the same notation.

#### Bryan Gin-ge Chen (Oct 10 2020 at 19:11):

(deleted, Pedro gave a better answer)

#### Pedro Minicz (Oct 10 2020 at 19:14):

{} is an empty "set comprehension," like {1, 2, 3} but with zero elements.

#### Pedro Minicz (Oct 10 2020 at 19:14):

Look at docs#is_lawful_singleton, it should give you an idea of what is happening behind the scenes.

#### Patrick Thomas (Oct 10 2020 at 19:15):

Is there any underlying definition somewhere for set comprehension?

#### Patrick Thomas (Oct 10 2020 at 19:16):

So it appears that a set is just a predicate?

#### Pedro Minicz (Oct 10 2020 at 19:16):

The notation {1, 2, 3} folds has_insert.insert with has_emptyc.emptyc.

#### Pedro Minicz (Oct 10 2020 at 19:16):

Yes, a set is just a predicate.

#### Pedro Minicz (Oct 10 2020 at 19:17):

{} is equal to ∅, which is equivalent to λ _, false.

#### Pedro Minicz (Oct 10 2020 at 19:19):

Pedro Minicz said:

The notation {1, 2, 3} folds has_insert.insert with has_emptyc.emptyc.

@Mario Carneiro is that correct? I can't seem to find a notation definition for  { l:(foldr ,  (x xs, insert x xs) ∅ }). Is it defined internally in C++?

#### Patrick Thomas (Oct 10 2020 at 19:20):

Does the following represent the proposition that a is a member of set s?

protected def mem (a : α) (s : set α) :=
s a


#### Pedro Minicz (Oct 10 2020 at 19:22):

Yes. Since sets are predicates (α → Prop) and a : α, s a : Prop, which is true or false depending on whether a "is in" s.

#### Bryan Gin-ge Chen (Oct 10 2020 at 19:24):

Pedro Minicz said:

I can't seem to find a notation definition for  { l:(foldr ,  (x xs, insert x xs) ∅ }). Is it defined internally in C++?

I think it's defined here: https://github.com/leanprover-community/lean/blob/master/src/frontends/lean/brackets.cpp

#### Pedro Minicz (Oct 10 2020 at 19:27):

Ah, yes, this looks like it.

#### Patrick Thomas (Oct 10 2020 at 19:33):

Would this be an equivalent definition: def singleton (α : Type) (a : α) (s : set α) := ∀ b : α, (set.mem b s) → b = a?

#### Patrick Thomas (Oct 10 2020 at 19:35):

Doesn't insert itself use the {} notation?

#### Pedro Minicz (Oct 10 2020 at 20:16):

set.insert uses { ... | ... } notation, which is different from {.., ..., ...}.

#### Pedro Minicz (Oct 10 2020 at 20:17):

set_option pp.notation false
#print set.insert -- λ {α : Type u} (a : α) (s : set α), set_of (λ (b : α), or (eq b a) (has_mem.mem b s))


If you disable notations when printing, you can see the definition of set.insert.

#### Pedro Minicz (Oct 10 2020 at 20:18):

Patrick Thomas said:

Would this be an equivalent definition: def singleton (α : Type) (a : α) (s : set α) := ∀ b : α, (set.mem b s) → b = a?

This is a predicate on sets. It says that the set s contains only one element.

#### Pedro Minicz (Oct 10 2020 at 20:21):

Sets are predicates on a type. Consider def singleton' (a : α) : set α := λ x, x = a, singleton' a is a set of α, that is, a predicate on α. While with your definition singleton a s says that s is a set that only contains a.

#### Patrick Thomas (Oct 10 2020 at 20:25):

That is what I was intending.

#### Patrick Thomas (Oct 10 2020 at 20:26):

That it was an equivalent definition to {a}.

#### Patrick Thomas (Oct 10 2020 at 20:48):

Wait, are you saying that singleton' is a set of alpha that only contains a?

#### Pedro Minicz (Oct 10 2020 at 20:51):

Yes, singleton' a is a set that only contains a.

#### Patrick Thomas (Oct 10 2020 at 21:23):

I guess I don't understand the difference between my def singleton (α : Type) (a : α) (s : set α) := ∀ b : α, (set.mem b s) → b = a and your def singleton' (a : α) : set α := λ x, x = a.

#### Patrick Thomas (Oct 10 2020 at 21:24):

Is it just that mine takes a set as a parameter?

#### Pedro Minicz (Oct 10 2020 at 21:34):

Observe the types of both definitions:

variable {α : Type}

def sing (a : α) (s : set α) : Prop :=
∀ b ∈ s, b = a

def sing' (a : α) : set α :=
-- Remember that set α = α → Prop.
λ b, a = b

variables (a : α) (s : set α)

#check sing a -- set α → Prop, that is, a predicate on set α.
#check sing' a -- set α, that is, a predicate on α.


#### Patrick Thomas (Oct 10 2020 at 21:36):

I see. Thank you.

#### Pedro Minicz (Oct 10 2020 at 21:36):

Your predicate talks about sets. It is true if and only if the set in question is a singleton set. My singleton' creates a set, that is, given an a : α it creates a predicate α → Prop.

#### Patrick Thomas (Oct 10 2020 at 21:43):

So...?

def union {α : Type} (s t : set α) : set α :=
λ x, (set.mem x s) ∨ (set.mem x t)


#### Pedro Minicz (Oct 10 2020 at 21:45):

Yes! That is exactly it!

Cool. Thank you!

#### Pedro Minicz (Oct 10 2020 at 21:46):

I'd recommend using x ∈ s as it is a bit easier to read than set.mem.

Ok.

#### Pedro Minicz (Oct 10 2020 at 21:47):

Also, since sets are predicates and predicates are functions, you can write λ x, s x ∨ t x to make what is happening under the hood explicit.

Cool.

#### Lúcás Meier (Dec 20 2020 at 17:33):

So, I've seen that Lean has a kind of set notation: {a : nat | a >= 3} (modulo unicode syntax). Is this hard-coded into the language, or could you define a similar kind of notation for other things?

It's hardcoded.

#### Mario Carneiro (Dec 20 2020 at 17:36):

but you can define similar notation, as long as you don't start with {

Last updated: May 09 2021 at 19:11 UTC