Abstraction in Equation

Stream: maths

[Ian Wood]

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]

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]

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]

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

[Yaël Dillies]

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]

f basically has the same role as ¬