Proof of Cantor Injective?

Stream: maths

[Joseph O]

Here is a proof of Cantor's theorem for surjective functions. Is there a similar document for the proof that for a set A, and a function f which takes in a subset of A and returns an element of A, f cant be injective?

[Riccardo Brasca]

I would do something like the following. Let $f \colon \mathcal{P}(A) \to A$ be injective. Let $B = \{X \subseteq A \text{ such that } f(X) \not \in X\}$ and consider $B' = \{ f(Y) \text { for } Y \in B \} \in \mathcal{P}(A)$. Now finish by considering the two cases $b \in B'$ or not.

[Joseph O]

is B a set of subsets?

[Riccardo Brasca]

Yes, I don't see any ambiguity in the notation. $B$ is the set whose elements are subsets $X \subseteq A$ such that $f(X) \not \in X$.

[Joseph O]

set B := {x : set α | x ⊆ α ∧ f x ∉ x},

Seems like a is supposed to be of type set a

[Riccardo Brasca]

You're again writing Lean code before having understood the math.

BTW since you have already proved that there are no surjective function in the other directions, you can prove, in general, that there a surjective $f \colon X \to Y$ iff there is an injective $$$g \colon Y \to X$.

[Joseph O]

Riccardo Brasca said:

You're again writing Lean code before having understood the math.

BTW since you have already proved that there are no surjective function in the other directions, you can prove, in general, that there a surjective $f \colon X \to Y$ iff there is an injective $$$g \colon Y \to X$.

Instead of proving cantor_injective?

[Joseph O]

Btw, if x is of type set α, is it necessary to say x ⊆ α

[Joseph O]

Like in the lean code

[Eric Wieser]

Note that this was already discussed in new members, so anyone replying here with lean code should probably read that first

[Eric Wieser]

Joseph O said:

Btw, if x is of type set α, is it necessary to say x ⊆ α

x ⊆ α is a type error. It is necessary to not say type errors.

[Joseph O]

Riccardo Brasca said:

I would do something like the following. Let $f \colon \mathcal{P}(A) \to A$ be injective. Let $B = \{X \subseteq A \text{ such that } f(X) \not \in X\}$ and consider $B' = \{ f(Y) \text { for } Y \in B \} \in \mathcal{P}(A)$. Now finish by considering the two cases $b \in B'$ or not.

Im a bit confused on how to show that B' is in $\mathcal{P}(A)$ in lean

[Joseph O]

My current translation of B' is

set B' := {y : α | ∃ x : set α, x ∈ B},

[Eric Wieser]

That's in 𝒫 A by definition

[Eric Wieser]

The goal view says B : set α, right?

[Joseph O]

yes

[Eric Wieser]

In type theory $\mathcal{P}(A)$ is often written set A

[Joseph O]

Yes I am aware of that, but doing set B' := {y : α | ∃ x : set α, x ∈ B} ∈ set α, doesn't give anything fruitful

[Joseph O]

Its failing to synthesize has_mem (set α) Type

[Joseph O]

Idea why?

[Joseph O]

Here is my proof so far:

theorem cantor_injective {α : Type} (f : set α → α) :
  ¬function.injective f :=
begin
  set B := {x : set α | f x ∉ x},
  set B' := {y : α | ∃ x : set α, f x = y ∧ x ∈ B},
  by_contradiction,
  have : ∃ (b : α), b ∈ B',
  { sorry, },
  { sorry, }
end

[Jireh Loreaux]

Drop the ∈ set α. Then it should work and in the infoview you should see B' : set α.

[Jireh Loreaux]

Can you fill those sorrys with a mathematical proof (not a Lean proof)?

[Joseph O]

My take on the first sorry is that b ∈ B' has the type α ∈ set α and that should be true?
Not sure how to put this into lean code

[Kyle Miller]

Here's an unobfuscated version of docs#function.cantor_injective

theorem cantor_injective {α : Type} (f : set α → α) :
  ¬function.injective f :=
begin
  intro i,
  let g : α → set α := λ a, { b | ∀ (s : set α), a = f s → b ∈ s },
  apply function.cantor_surjective g,
  have : function.right_inverse f g,
  { intro s,
    ext a,
    split,
    { intro h,
      apply h,
      refl, },
    { intros h' s' e,
      specialize i e,
      cases i,
      exact h' } },
  exact function.right_inverse.surjective this,
end