# Zulip Chat Archive

## 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`

?

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

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.

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

#### 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 },
contradiction, },
{ have : x ∈ f x,
{ rwa hx, },
contradiction, },
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