Setting up exercises for cardinality on Sets

Stream: new members

[Derek Rhodes]

Hi all, I'm exploring a template for exercises about cardinality on sets. My goal has shifted from "staying as close to the learning material as possible (which like most math resources use set theory)" over to "use Mathlib to the extent possible without frying people's brains, my own included". To that end, if possible, I think it would be good to use a template. This was my first stab at it, but I don't like it

import Mathlib

open Cardinal

def A : Set ℤ := sorry
def B : Set ℤ := sorry

noncomputable
def bijection : ↑A ≃ ↑B := by sorry

theorem card_a_eq_card_b : #A = #B := mk_congr bijection

So, after more experimenting, found what seems to be a less noisy approach:

import Mathlib

namespace Template
open Function Set Cardinal
-- 3(a) Let A and B be two disjoint, countably infinite sets. Prove that A ∪ B is
-- countably infinite.

def A := { m : ℕ | Even m }
def B := { n : ℕ | Odd n }
def C := A ∪ B

example : #C = ℵ₀ := by
  have : Infinite C := by
    -- this looks like a promising route.
    sorry
  apply mk_eq_aleph0 ↑C -- scary?

end Template

Maybe someone has a better idea for how to introduce cardinality to people who are just getting their toes wet with Mathlib? I'd also like to see any documentation about it. "The Mechanics of Proof" stops short of it. "Formalizing Math" doesn't seem to cover it. "Mathematics in Lean" mentions it in passing, "How to Prove it" doesn't cover it. Did I miss any, are there any other math focused lean4 books?

[Dan Velleman]

How To Prove It With Lean does cover cardinality, but not by using anything in Mathlib. Rather, it defines everything from scratch. It includes the following theorems: a countable union of countable sets is countable, the power set of the natural numbers is uncountable, and the Cantor-Schroeder-Bernstein theorem.

[Derek Rhodes]

I guess I'm really looking for how to do it with the Mathlib structures, for whatever reason it seems like there is a cliff in abstraction at cardinality. I'm have trouble finding a path to Bijection from #C = ℵ₀ Maybe there is a lemma .._iff_.. to Bijection specialized for Set.

[Kyle Miller]

I'm not sure if this is an artifact of making a MWE, but in exercise 3(a) you're not allowed to choose your own disjoint countably infinite sets — you're supposed to prove this for arbitrary ones.

[Derek Rhodes]

Yep :) I was just doing a concrete example to get started

[Kyle Miller]

That's going to potentially be very misleading, since with your choice C is Set.univ. You don't want to accidentally use any specific properties of your choices.

[Kyle Miller]

If you want to encode countably infinite using cardinality, here's something to get started with:

example {α : Type _} (A B : Set α) (hDisj : A ∩ B = ∅)
    (hA : #A = ℵ₀) (hB : #A = ℵ₀) : #C = ℵ₀ := by
  sorry

[Derek Rhodes]

Thank you, that's helpful, but the hurdle I'm currently facing is cracking the #C = ℵ₀ into a Bijection.

[Kyle Miller]

Have you tried setting up an example with the givens and what you want and using exact? ?

[Derek Rhodes]

yeah, exact?, apply?, which offers a flood of avenues to explore.

[Derek Rhodes]

None of them are particularly beginner friendly, with Bijection, which people would be familiar with.

[Kyle Miller]

(It looks like docs#Cardinal.eq is how you're supposed to go from equal cardinalities to equivalent types.)

[Kyle Miller]

example (α : Type) (h : #α = ℵ₀) : Nonempty (α ≃ ℕ) := by
  rw [← Cardinal.mk_nat, Cardinal.eq] at h
  exact h

[Derek Rhodes]

That looks really promising, a good place to start hacking. Thank you.

[Marco Campos]

Quick question that I think pertains to Derek's message prior to this. When I use apply? , I don't typically get suggestions for tactics that I want to use at least for my current level. Is there another command that lets me suggest commands that specifically apply to a certain library such as giving me a display of theorems in Cardinal for example without consulting the docs in the browser or using something like Lean Copilot? I'm just curious if there was an option in the editor that already exists

[Ruben Van de Velde]

Note that exact?, apply?, rw? all look for theorems that work with the tactic with the ? stripped - they don't look for tactics. hint is an example of a tactic that looks for other tactics to try.

[Ruben Van de Velde]

Possibly

#loogle Cardinal

is helpful?