cardinality proofs with lean/mathlib

Stream: new members

[rzeta0]

If I continue learning lean/mathlib, would I eventually be able to do cardinality proofs?

Examples:

• Prove the cardinality of the set of natural numbers is the same as the set of integers.

• Prove the cardinality of the set of natural number is not the same a the set of reals.

• Prove the cardinalty of the set $(A^B)^C$ is the same as the set $A^{B \times C}$, where $Y^X$ is the powerset of all functions from $X \to Y$

That last one is something I've struggled to do as I work my way through a maths textbook, and wonder if the discipline of lean might help clarify my thinking (just as unique existence proofs did recently)

I'm just wondering what mathlib might provide to help such proofs.

[Kyle Miller]

• docs#Cardinal.mk_int
• basically https://github.com/leanprover-community/mathlib4/blob/549f950ffa3478a7c5c62c31b940ed4b01ef268d/Mathlib/Data/Real/Cardinality.lean#L202-L205
• example (α β γ : Type*) : Cardinal.mk (α × β → γ) = Cardinal.mk (α → β → γ) := Cardinal.mk_congr (Equiv.curry α β γ)

[Derek Rhodes]

From a far more basic perspective, (I've only taken applied math courses formally in school and am now learning pure math by learning lean and currently working through real analysis), I found that building the definitions required for doing simple cardinality proofs in the language of the course, from scratch, was easier than using the Mathlib defs. For example, here is a proof that the cardinality of a set $A$ is less than the cardinality of the powerset of $A$. (It's not as elegant, abstract or general as what is in mathlib, but it works!) (edited to fix definition and proof)

import Mathlib.Tactic

def inj (A: Set α) (B: Set β) (f: α→β) := ∀x ∈ A, ∀y ∈ A, (f x ∈ B) ∧ (f y ∈ B) ∧ f x = f y → x = y
def sur (A: Set α) (B: Set β) (f: α→β) := ∀y ∈ B, ∃x ∈ A, f x ∈ B ∧ f x = y
def bij (A: Set α) (B: Set β) (f: α→β) := inj A B f ∧ sur A B f

def card_eq (A: Set α) (B: Set β) := ∃ f, bij A B f
def card_le (A: Set α) (B: Set β) := ∃ f, inj A B f
-- def card_lt (A: Set α) (B: Set β) := ∃ f, inj A B f ∧ ¬ bij A B f -- (wrong)
def card_lt (A: Set α) (B: Set β) := ∃ f, inj A B f ∧ ¬ card_eq A B -- fixed.

open Set

theorem cantor (A: Set α) : card_lt A (powerset A) := by
  use (λ x => {x}) -- choose some f where f(x) = {x}
  constructor
  · -- inj A (𝒫 A) fun x ↦ {x}
    intro x hx y hy h
    obtain ⟨_, _, h₁⟩ := h
    dsimp at *
    rw [←singleton_eq_singleton_iff]
    exact h₁
  · -- |A| ≠ |𝒫 A|
    by_contra h
    dsimp [card_eq] at h
    obtain ⟨g, hg⟩ := h

    let B := {x ∈ A | x ∉ g x}
    have hb : B ∈ 𝒫 A := @mem_of_mem_diff α A (λ x => g x x)

    obtain ⟨h₁, h₂⟩ := hg
    rw [sur] at h₂

    have hg : ∃ b ∈ A, g b = B := by
      obtain ⟨x, ⟨hx₁, _, hx₂⟩⟩ := h₂ B hb
      use x

    obtain ⟨b, ⟨hb₁, hb₂⟩⟩ := hg

    cases (Classical.em (b ∈ g b)) with
    | inl h =>
      · have hc := h
        dsimp [B] at hb₂
        rw [hb₂] at h
        obtain ⟨_, hc₂⟩ := h
        contradiction
    | inr h =>
      · have hc := h
        dsimp [B] at hb₂
        rw [hb₂] at h
        simp at h
        have := h hb₁
        contradiction

Also, if you haven't found them yet, the Formalizing Mathematics videos and worksheets use Mathlib directly and contain a lot of hard fought wisdom.

[Dan Velleman]

@Derek Rhodes Your definition of card_lt is not correct. It is not good enough to say that there is an injection that is not a bijection. You have to say there is an injection, and there is no function that is a bijection. For example, consider the function $f$ from the natural numbers to the natural numbers defined by $f(n) = n + 1$. That function is an injection but not a bijection, so by your definition you would end up concluding that the natural numbers are smaller than themselves, which is wrong.

[Derek Rhodes]

Thanks for taking the time to review my proof, I appreciate it and will try to fix it.

[Dan Velleman]

Also, there is a slight technicality concerning the empty set. Suppose α is a nonempty type and β is an empty type. Then there is no function from α to β. But the empty sets of those two types should have the same cardinality. The problem is caused by the fact that you use functions f : α → β, so f must assign a value to every object of type α--even those that are not elements of A, so values are not needed for them. As long as β is nonempty it is possible to assign those values, so there won't be a problem. But if you try to prove theorems about cardinality using your definitions, occasionally you may run into situations in which you need to add a hypothesis that β is nonempty.

In How To Prove It with Lean, I took a similar approach, but I used relations rather than functions to avoid this technicality concerning unneeded values. Cardinalities are covered in Chapter 8.
The proof of Cantor's theorem is at the end of Section 8.2.

[Derek Rhodes]

@Dan Velleman, thanks again for the valuable feedback, I'm glad you're here to point out these gotchas and will work through chapter 8 to see if I can make better sense of things.

[Dan Velleman]

Unfortunately, it may be difficult to just jump into Chapter 8. I use a "dialect" of Lean that is somewhat different from standard Lean, so you may have to read earlier parts of the book to learn that dialect.