## Stream: general

### Topic: How does this proof work?

#### Joseph O (May 04 2022 at 00:37):

I have this proof, and for the second line, library_search suggested exact singleton_injective, and it closed off the whole proof, and I looked at the definition, and wasn't able to understand why

theorem cantor_theorem {α : Type} (f : α → set α) : # α ≤ # (set α) :=
begin
apply mk_le_of_injective,
exact singleton_injective,
end


#### Scott Morrison (May 04 2022 at 00:41):

It seems pretty straightforward. Perhaps you could try describing (in English) the type signatures of mk_le_of_injective and singleton_injective, and see if by the time you've done that it makes sense?

#### Scott Morrison (May 04 2022 at 00:41):

Have you looked at the goal after the apply statement?

#### Scott Morrison (May 04 2022 at 00:42):

Also, please try to post a #mwe (that is a clickable link). You're much more likely to get helpful answers if others can copy and paste your code block into a new file and have it work immediately.

#### Eric Wieser (May 04 2022 at 00:42):

Didn't you already ask this here?

#### Scott Morrison (May 04 2022 at 00:42):

(Here you are missing an import statement, and open_locale, and two opens.)

#### Joseph O (May 04 2022 at 00:44):

Eric Wieser said:

Didn't you already ask this here?

No?

#### Joseph O (May 04 2022 at 00:44):

Scott Morrison said:

It seems pretty straightforward. Perhaps you could try describing (in English) the type signatures of mk_le_of_injective and singleton_injective, and see if by the time you've done that it makes sense?

wait is single_injective a singleton map?

#### Joseph O (May 04 2022 at 00:45):

Is it describing this?
There exists an injection from $S$ to $\mathcal{P}S$, given by the singleton map.

#### Eric Wieser (May 04 2022 at 00:48):

Why don't you look at docs#set.singleton_injective to find out?

#### Eric Wieser (May 04 2022 at 00:48):

And if you don't understand the statement, then click on the pieces of it (recursively) until you do

#### Scott Morrison (May 04 2022 at 00:49):

Maybe post here your attempts at translating the type signature of singleton_injective into English (=informal maths)...

#### Joseph O (May 04 2022 at 00:49):

Eric Wieser said:

Why don't you look at docs#set.singleton_injective to find out?

Yeah and it seems exactly like that statement.

#### Joseph O (May 04 2022 at 00:50):

Scott Morrison said:

Maybe post here your attempts at translating the type signature of singleton_injective into English (=informal maths)...

singleton_injective says the function from a an element of a set a to a subset is injective. Or, in other words, there exists an injective function from a set to its powerset

No

#### Scott Morrison (May 04 2022 at 00:50):

Or at least, what do you mean by "the function".

#### Scott Morrison (May 04 2022 at 00:51):

It's certainly not an existential statement.

#### Joseph O (May 04 2022 at 00:56):

Scott Morrison said:

Or at least, what do you mean by "the function".

Let me try again: the singleton map from a set and its poweset is injective

Last updated: Dec 20 2023 at 11:08 UTC