## Stream: new members

### Topic: Constructing Sets and Powersets

#### Georgio Nicolas (Mar 02 2022 at 16:52):

Hello :-)

I'm trying to reason about Sets, Powersets, and their elements in Lean.
If someone can help me construct the following I would be eternally grateful.

Definitions:
x, y, z, w: elements of some Type U
A: set of Type U such that A = {x,y,z}
PA: The powerset of A

A decision function (U -> set U -> \N) which checks if an element of U is an element of A and returns 1/0

A decision function (set U -> set (set U) -> \N) which checks if an element of set U is an element of set (set U) and returns 1/0

Goal (using the 2 functions):

1. Prove that x is an element of A
2. Prove that w is not an element of A
3. Prove that {x, y} is an element of PA

I am currently stuck at the definitions, but here's some code in case it would be helpful:

import data.set
open set

variable {U : Type}
variables x y z w : U
def A : set U := {x, y, z}

#print A

--- --- It seems that A is not of the right type
def PA : set (set U) := powerset A


#### Georgio Nicolas (Mar 02 2022 at 16:55):

I will be making some edits to make my message more legible but won't be changing the content

#### Riccardo Brasca (Mar 02 2022 at 16:57):

You have produced a function, called A, that given three elements x y z of U, produces the set with these three elements. So the set you want is  A x y z.

#check A x y z --A x y z : set U


#### Riccardo Brasca (Mar 02 2022 at 17:00):

In practice you can always directly write ({x, y, z} : set U).

#### Georgio Nicolas (Mar 02 2022 at 17:02):

Thank you very much for the tip

#### Riccardo Brasca (Mar 02 2022 at 17:04):

Depending on what you are doing it's possible that Lean can guess the  : set U part.

#### Georgio Nicolas (Mar 02 2022 at 17:08):

Can I store that as a hypothesis?

Riccardo Brasca said:

In practice you can always directly write ({x, y, z} : set U).

#### Georgio Nicolas (Mar 02 2022 at 17:09):

variable A : ({x, y, z} : set U)
#check A --- A : ↥{x, y, z}


#### Georgio Nicolas (Mar 02 2022 at 17:09):

I'm sorry I'm a complete beginner

#### Patrick Massot (Mar 02 2022 at 17:11):

What did you read so far to learn Lean?

#### Riccardo Brasca (Mar 02 2022 at 17:12):

You can use parameters for that, but this can be a little problematic. If you just want to avoid typing ({x, y, z} : set U) a lot, you can just write

local notation A := ({x, y, z} : set U)


So now typing A is literally the same as typing ({x, y, z} : set U) (in the current file).

#### Patrick Massot (Mar 02 2022 at 17:12):

It seems you would benefit a lot from reading more before trying to do things of your own.

#### Yaël Dillies (Mar 02 2022 at 17:12):

or set A : set U := {x, y, z} within a tactic block

#### Georgio Nicolas (Mar 02 2022 at 17:13):

I'm going through the Mathematics in Lean tutorial, I'm done with part 2

#### Georgio Nicolas (Mar 02 2022 at 17:14):

Riccardo Brasca said:

You can use parameters for that, but this can be a little problematic. If you just want to avoid typing ({x, y, z} : set U) a lot, you can just write

local notation A := ({x, y, z} : set U)


So now typing A is literally the same as typing ({x, y, z} : set U) (in the current file).

This is exactly what I needed!!! Thank you so much

#### Patrick Massot (Mar 02 2022 at 17:16):

What do you call part 2? Is it https://avigad.github.io/mathematics_in_lean/02_Basics.html ?

Yes

#### Georgio Nicolas (Mar 02 2022 at 17:17):

Seems like a long way to go

#### Georgio Nicolas (Mar 02 2022 at 17:17):

Maybe I'm trying to jump forward

#### Georgio Nicolas (Mar 02 2022 at 17:17):

But I will complete it

#### Patrick Massot (Mar 02 2022 at 17:18):

I strongly recommend you also go through parts 3 and 4 before returning to what you're currently doing.

#### Georgio Nicolas (Mar 02 2022 at 17:18):

Okay I will, thanks again

#### Patrick Massot (Mar 02 2022 at 17:20):

@Jeremy Avigad do we have a clear plan about when we plan to discuss subtype and the ↥ arrow so that people at least recognize it when they don't actually want it?

#### Jeremy Avigad (Mar 02 2022 at 17:28):

First, a note: the "official" (at least, more official -- it's still evolving and growing) version of MIL is https://leanprover-community.github.io/mathematics_in_lean/. The avigad version is used to test and share drafts of new sections.

That said, subtypes are mentioned in passing at the end of the draft section here: https://avigad.github.io/mathematics_in_lean/06_Abstract_Algebra.html#structures.
That seemed a natural place to mention their existence, but I wasn't planning to say much about them. I am open to suggestions, though.

#### Patrick Massot (Mar 02 2022 at 17:52):

I think it would be nice to mention them in the section on sets.

#### Jeremy Avigad (Mar 02 2022 at 17:56):

Just say that they exist and can be used to turn a set or a property into a new type? With a forward reference to the later section?

#### Patrick Massot (Mar 02 2022 at 17:57):

And also a warning saying that if readers suddenly see the ↥ arrow appearing then it means they inadvertently used this concept and they should think harder.

#### Jeremy Avigad (Mar 02 2022 at 18:53):

Will do!

Last updated: Dec 20 2023 at 11:08 UTC