Zulip Chat Archive

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 ?

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

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