Zulip Chat Archive

Stream: maths

Topic: Abstraction in Equation


Ian Wood (Jun 26 2021 at 10:12):

Essentially I'm trying to do Cantor's diagonal argument, and I've gotten close:

open function

lemma diagonal_argument {α : Type*} (f : α  α) (h : x, x  f x) : ¬∃(g :   (  α)), surjective g :=
begin
  intro h,
  cases h with g g_sur,
  unfold surjective at g_sur,
  have diagonal_new, from g_sur (λ n, f (g n n)),
  cases diagonal_new with m g_n,
  suffices : g m m = f (g m m), from h _ this,
  sorry,
end

Currently at sorry I have the goal:

α : Type u_1,
f : α  α,
h :  (x : α), x  f x,
g :     α,
g_sur :  (b :   α),  (a : ), g a = b,
m : ,
g_n : g m = λ (n : ), f (g n n)
 g m m = f (g m m)

Unless I'm mistaken I should be able to apply m to both sides, as g m is a sequence of alphas, and λ (n : ℕ), f (g n n) is definitionally equal. Can I do this, and if so how?

Yaël Dillies (Jun 26 2021 at 10:15):

I do not really get what you're trying to do. Are you trying to show that there's no surjective function from X to its powerset?

Ian Wood (Jun 26 2021 at 10:18):

Given a function that can "change" one alpha to a different alpha (like in the example of showing reals are uncountable, would be 0 -> 1, 1 -> 2, ... 9 -> 0), there cannot be a surjective mapping from naturals to infinite sequences of alphas (eg there cannot be a list of all real numbers between 0 and 1), because if there was we can create a new sequence that wasn't taken into account.

Ian Wood (Jun 26 2021 at 10:19):

Also I didn't realise this wasn't new members, sorry.

Yaël Dillies (Jun 26 2021 at 10:22):

Ah I see. But the only point of your function is to show that α has at least two elements. So I would suggest to abstract it away for now and first try proving

lemma diagonal_argument {α : Type*} (g : α  α  Prop) (hg : surjective g) : false := sorry

Yaël Dillies (Jun 26 2021 at 10:25):

f basically has the same role as ¬


Last updated: Dec 20 2023 at 11:08 UTC