Constructing Sets and Powersets

Stream: new members

[Georgio Nicolas]

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]

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

[Riccardo Brasca]

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]

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

[Georgio Nicolas]

Thank you very much for the tip

[Riccardo Brasca]

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

[Georgio Nicolas]

Can I store that as a hypothesis?

Riccardo Brasca said:

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

[Georgio Nicolas]

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

[Georgio Nicolas]

I'm sorry I'm a complete beginner

[Patrick Massot]

What did you read so far to learn Lean?

[Riccardo Brasca]

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]

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

[Yaël Dillies]

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

[Georgio Nicolas]

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

[Georgio Nicolas]

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]

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

[Georgio Nicolas]

Yes

[Georgio Nicolas]

Seems like a long way to go

[Georgio Nicolas]

Maybe I'm trying to jump forward

[Georgio Nicolas]

But I will complete it

[Patrick Massot]

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

[Georgio Nicolas]

Okay I will, thanks again

[Patrick Massot]

@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]

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]

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

[Jeremy Avigad]

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]

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]

Will do!