Zulip Chat Archive
Stream: new members
Topic: Setting up exercises for cardinality on Sets
Derek Rhodes (Jan 04 2025 at 20:41):
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 (Jan 04 2025 at 20:53):
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 (Jan 04 2025 at 21:02):
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 (Jan 04 2025 at 21:06):
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 (Jan 04 2025 at 21:07):
Yep :) I was just doing a concrete example to get started
Kyle Miller (Jan 04 2025 at 21:08):
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 (Jan 04 2025 at 21:08):
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 (Jan 04 2025 at 21:12):
Thank you, that's helpful, but the hurdle I'm currently facing is cracking the #C = ℵ₀
into a Bijection.
Kyle Miller (Jan 04 2025 at 21:15):
Have you tried setting up an example
with the givens and what you want and using exact?
?
Derek Rhodes (Jan 04 2025 at 21:15):
yeah, exact?
, apply?
, which offers a flood of avenues to explore.
Derek Rhodes (Jan 04 2025 at 21:16):
None of them are particularly beginner friendly, with Bijection, which people would be familiar with.
Kyle Miller (Jan 04 2025 at 21:21):
(It looks like docs#Cardinal.eq is how you're supposed to go from equal cardinalities to equivalent types.)
Kyle Miller (Jan 04 2025 at 21:24):
example (α : Type) (h : #α = ℵ₀) : Nonempty (α ≃ ℕ) := by
rw [← Cardinal.mk_nat, Cardinal.eq] at h
exact h
Derek Rhodes (Jan 04 2025 at 21:26):
That looks really promising, a good place to start hacking. Thank you.
Marco Campos (Jan 04 2025 at 22:30):
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 (Jan 04 2025 at 22:54):
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 (Jan 04 2025 at 22:55):
Possibly
#loogle Cardinal
is helpful?
Last updated: May 02 2025 at 03:31 UTC