## Stream: new members

### Topic: No surjection from a set to its powerset

#### Gihan Marasingha (Oct 26 2020 at 14:19):

I know mathlib has the theorem cantor_surjective, that given {α} (f : α → set α), we have ¬ function.surjective f. Can one prove a similar statement given (S : set α) (f : S → 𝒫 S)?

I've attempted this, but I come a cropper because I'm trying apply surjectivity to a term of the wrong type. Here's the start of my attempt. The problem is that I'm applying h with a term of type set ↥S rather than one of type ↥𝒫 S. Can this be fixed?

import data.set

example {α} (S : set α) (f : S → 𝒫 S) : ¬ function.surjective f :=
begin
haveI := classical.prop_decidable,
intro h,
cases h { b : S | (b : α) ∉ (f b : set α)} with x hx, -- This fails.
/-  by_cases k : x ∈ f x,
{ have : x ∉ f x,
{ rwa [hx, nmem_set_of_eq, not_not_mem], },
exact this k, },
{ have : x ∈ f x,
{ rwa [hx, mem_set_of_eq], },
exact k this, }, -/
end


#### Mario Carneiro (Oct 26 2020 at 14:20):

why not just turn it into an instance of cantor_surjective?

also #mwe

#### Gihan Marasingha (Oct 26 2020 at 14:23):

Ah sorry, I've added the import.

#### Gihan Marasingha (Oct 26 2020 at 14:25):

OK, so how would I apply cantor_surjective in this case to get the desired result?

#### Mario Carneiro (Oct 26 2020 at 14:27):

def equiv.set.powerset {α} (S : set α) : 𝒫 S ≃ set S := sorry


#### Gihan Marasingha (Oct 26 2020 at 14:38):

Thanks. I haven't come across equiv before. I'll think about this and come back if I get stuck.

#### Kevin Buzzard (Oct 26 2020 at 15:33):

When I do this with Imperial 1st years I just use types:

import data.set

open_locale classical

open set

example (S : Type) (f : S → set S) : ¬ function.surjective f :=
begin
intro h,
cases h { b : S | b ∉ f b} with x hx,
by_cases k : x ∈ f x,
{ have : x ∉ f x,
{ rw hx at k, exact k },
{ have : x ∈ f x,
{ rwa hx, },
end


#### Kevin Buzzard (Oct 26 2020 at 15:34):

I just tell them that a type is a collection of stuff in type theory, like a set is a collection of stuff in set theory.

#### Mario Carneiro (Oct 26 2020 at 15:40):

Although I think it is interesting how shockingly short the mathlib proof of cantor_surjective is

#### Gihan Marasingha (Oct 26 2020 at 15:40):

@Kevin Buzzard . Thanks. I feel less bad about trying a classical proof (given that function.cantor_surjective is constructive).

#### Mario Carneiro (Oct 26 2020 at 15:41):

it actually uses that ever popular lemma from TPIL that is not obviously constructive: not (p <-> not p)

#### Gihan Marasingha (Oct 26 2020 at 15:42):

Oh, good to know! I take it then the result is not true using constructive reasoning?

Edit: I can't read. Ignore this comment.

#### Kevin Buzzard (Oct 26 2020 at 15:42):

not (p <-> not p) can be proved constructively, rather surprisingly

#### Gihan Marasingha (Oct 26 2020 at 16:01):

@Kevin Buzzard when teaching do you avoid discussing power sets entirely (treating set S as a 'power type') or do you discuss power sets then ask students to think of set S (in this situation) as being a power set? Or something else?

#### Mario Carneiro (Oct 26 2020 at 16:02):

I don't think set.powerset has been used at all in mathlib

#### Mario Carneiro (Oct 26 2020 at 16:03):

Once you have a separate notion of the type of subsets of a type, there are very few instances where the subcollection of subsets of a given subset of a type comes up

#### Gihan Marasingha (Oct 26 2020 at 16:05):

@Mario Carneiro. Trying to prove this non-surjectivity result for power sets, I can see why!

#### Mario Carneiro (Oct 26 2020 at 16:06):

Well in this case you aren't really using set.powerset as a set, so the translation to set S is natural

#### Kevin Buzzard (Oct 26 2020 at 16:06):

I say that set S is the type of subsets of S, and the reason it's not called subset S is because a term of type set S is a set of elements of S.

#### Mario Carneiro (Oct 26 2020 at 16:06):

There are uses of set.prod in mathlib (the cartesian product of sets), so conceivably a similar thing might come up for set.powerset

#### Yury G. Kudryashov (Oct 26 2020 at 16:08):

docs#filter.eventually_lift'_powerset

#### Mario Carneiro (Oct 26 2020 at 16:09):

oh that's right, filters will need this sometimes

#### Mario Carneiro (Oct 26 2020 at 16:09):

I went looking for uses of the notation

#### Mario Carneiro (Oct 26 2020 at 16:13):

Hm, should we use Iic instead of set.powerset?

#### Mario Carneiro (Oct 26 2020 at 16:13):

that would allow us to unify it with the collection of supersets {x | S \sub x}, which also comes up in filters

#### Yury G. Kudryashov (Oct 26 2020 at 16:20):

I'm not going to do this refactor!

#### Mario Carneiro (Oct 26 2020 at 17:00):

I can lump it in with that refactor I never finished to generalize filters to subsets of a poset

#### Johan Commelin (Oct 26 2020 at 17:03):

I fear that refactor might be really painful. Don't you think?
The fact that filters are filters on set X is really used all over the place now.
Not saying that it can't be done, but I think it might be one of the biggest refactors we've seen so far.

#### Mario Carneiro (Oct 26 2020 at 17:39):

You are not wrong

#### Mario Carneiro (Oct 26 2020 at 17:40):

It was one of those refactors where the size of the refactor grows exponentially with the number of touched theorems

Last updated: May 16 2021 at 20:13 UTC