Confused by the hint in 3.6.12

Stream: Analysis I

[Dan Abramov]

I read this several times and struggle to parse it:

Screenshot 2025-09-08 at 04.28.10.png

How can "a permutation φ : {i ∈ N : 1 ≤ i ≤ n++} → {i ∈ N : 1 ≤ i ≤ n}" make sense if we have 1 ≤ i ≤ n++ before the arrow but 1 ≤ i ≤ n after the arrow? This reads like Fin (n+1) → Fin n to me but then how can we call it a permutation (which has a type like Bijective Fin n → Fin n)?

[Dan Abramov]

Also, does "from the set" mean the same as "of the set" here or something different?

[Dan Abramov]

Maybe the right side should say 1 ≤ i ≤ n++ too?

[Terence Tao]

Ugh, the text got mangled here for some reason. Yes, both sets should involve n++ instead of n, and the clause "from the set {i in N: 1 \leq i \leq n++}" should be $S_{n++}$. (And of course the parentheses should be closed up.) This by the way is listed in the errata at https://terrytao.wordpress.com/books/analysis-i/

[Rado Kirov]

Yeah, the extra math notation do make the sentence a bit awkward even with the typos fixed.

Also, does "from the set" mean the same as "of the set" here or something different?

it reads

partition S into x subsets, depending on the value \phi(y) a permutation \phi from the set S assigns to y

for some specific S, x, y and more expanded type for \phi

So, yes, I think permutation of set X or permutation from set X (implicitly to X) mean the same thing.

[Dan Abramov]

Ahh, I didn't scroll down the errata enough (assumed it's all sorted by page). This is page 62 if you'd like to add that (errata currently says Page ???):

Screenshot 2025-09-08 at 10.05.48.png

[Dan Abramov]

I'm working through this exercise and I'm still not sure how to interpret the hint.

The idea I'm trying to go with is:

For each f: Permutations (n + 1), take f n (for the left part of the product). For the right side of the product, we need to produce f' : Permutations n. We do this by taking the original function f and restraining its domain to exclude n. This by itself would give us a function Fin n -> Fin (n+1) \ {f n}. To "repair" its codomain, we reroute whichever x previously pointed at n to the hole left by excluding f n. Then we'd need to make an inverse that does the opposite of this rerouting, and to prove that it's actually an inverse.

However, this already feels quite annoying (with lots of justifications for messing with Fins). I was wondering whether the hint in the text implies some more convenient approach — either for constructing the inner bijection (proving "the rerouting" gives us a bijective function), or for constructing the outer bijection (that this mapping between Permutations (n+1) and the product with our function is itself bijective).

In particular I'm not sure what's meant by partitioning the set in the hint, and how that helps here.

[Terence Tao]

This approach - setting up a bijection between Permutations (n+1) and Fin (n+1) × (Permutations n) - will work. The hint suggests a very slightly different approach, in which one partitions Permutations (n+1)into n+1 disjoint subsets, each of which is separately in bijection with Permutations n; these may end up having slightly different Lean formalizations but at a conceptual level they are nearly identical.

[Rado Kirov]

This approach - setting up a bijection between Permutations (n+1) and Fin (n+1) × (Permutations n) - will work.

Yep, that's what I did. Honestly, I wasn't even sure how to create a family of disjoint partitions and prove they are disjoint and union to the whole set, because there were not earlier exercises along these lines. But there were plenty of show cardinalities are equal by explicit bijection so my brain was biased.

Btw, it just came to me that I can remove all the surjective directions since those are fns from Fin n to Fin n, so injective implies surjective. Now the proof is 200 lines shorter and Lean no longer chokes on it - https://github.com/rkirov/analysis/commit/c1018dba173b903a49d0bbc913e888d8b8be7d0c . Tons of room for improvement left.

[Dan Abramov]

Where I’m not following along is how does partitioning into disjoint subsets help. Is it because we could then “add them up” one by one and thus we don’t need to construct the outer bijection explicitly? But then we’d need a lemma to repeatedly do card_union_disjoint. Or is there something else I’m missing about how to construct the big bijection from partition bijections?

[Dan Abramov]

If that’s the intended approach, maybe it would be nice to stub out some intermediate lemma about cardinality of a union of distinct sets

[Terence Tao]

Well, the problem was initially written for informal mathematics rather than for Lean, in which the concept of iterating the identity about cardinality of two disjoint sets to an arbitrary finite collection of disjoint sets would be considered "obvious". But for the purposes of creating a Lean proof, an alternate hint may be better - feel free to add one based on your solutions in the docstring of the problem, or in the general "tips" section at the start of the file.

[Rado Kirov]

If that’s the intended approach, maybe it would be nice to stub out some intermediate lemma about cardinality of a union of distinct sets

If you go that route you want something like

theorem SetTheory.Set.card_iUnion_of_pairwise_disjoint {n: ℕ} {X: Set} (S : Fin n → Set)
    (h_sub: ∀ i, S i ⊆ X)
    (h_disj : ∀ i, ∀ j, i ≠ j → Disjoint (S i) (S j))
    (h_complete: (Fin n).iUnion S = X)
    (h_finite : ∀ i, (S i).finite) :
    X.card = ∑ i, (S i).card := by
  sorry

But we never used \sum so far, and never make \sum support our custom Fin n. Ultimately, I am not even sure if the proof going this route is that much simpler than the explicit bijection that I did.

[Dan Abramov]

Thanks, that signature is helpful. I wasn't able to prove that one (I think we'd need Finset-like machinery for it) but I did manage to prove this:

theorem SetTheory.Set.card_iUnion_card_disjoint {n m: ℕ} (S : Fin n → Set)
    (hSc : ∀ i, (S i).has_card m)
    (hScd : Pairwise fun i j => Disjoint (S i) (S j)) :
    ((Fin n).iUnion S).finite ∧ ((Fin n).iUnion S).card = n * m := by

I haven't looked closely at whether it actually "helps" 3.6.12 but I'll give a try later.

[Dan Abramov]

I've managed to complete the exercise (in a week) but the code is very ugly. The construction I went with initially (swapping items) was too complicated because I had to by_cases on a bunch of conditions. So I'm redoing it now with a "shift by one" strategy.

I also found that the shape of the argument of showing the bijection, when following the path of least resistance ("whatever the goal says"), obscures what's happening. I'm sure there must be a much more concise way to talk about this. I've only yesterday realized that Permutations n is really just an Equiv (Fin n) (Fin n) (aka Equiv.Perm (Fin n)) in Mathlib terms. And what we're trying to establish is sort of an equivalence between equivalences — something like {f : Fin (n+1) ≃ Fin (n+1) // f n' = i} ≃ (Fin n ≃ Fin n).

So I'll try to redo my solution while following this "nested equivalences" structure which I expect to be much more legible.

Annoyingly, the argument in my head is even more concise than what I'm writing. In my head, I split the original bijective function in two (based on whether the output is larger than i index of S i), they're both obviously bijective, then I apply a x => x - 1 transformation to one of those slices (which is bijective so preserves the bijectivity), then I "glue" them together (and since their codomains don't overlap, the glued function also remains bijective). This transformation itself is a sequence of applying bijections, therefore it must also somehow be bijective and should be possible to apply in reverse.

I suspect there's some very short way to write this armed with Mathlib idioms around Fin and Equiv. Mathlib has succAbove and predAbove for Fin which seem relevant, or maybe sumCompl or something for splitting and gluing equivalences.

For now I'll see if writing nested equivalences explicitly simplifies the argument from my original form.

[Dan Abramov]

OK I have pretty good progress on this, should be able to PR some scaffolding I found useful in the next few days.

[Rado Kirov]

Nice, looking forward to the scaffolding and will give it some playtesting.

Mathematically, what you are describing makes sense, but I wonder if the Lean types will make this messier / awkward. The already provided solution card_erase also deals with "the create a new function with all images after f n shifted down) https://github.com/teorth/analysis/blob/main/analysis/Analysis/Section_3_6.lean#L93-L112 , so I styled my solution around that same method.

If you instead split the original permutation, into two bijections: ones that map to images before f n and ones that map to after f n, you will have bijections (hence Equivs of sets), but the domains are no longer describable well (they some random sets that union to all of Fin n + 1). Anyways, sounds like you made it work, so looking forward to seeing it.

[Dan Abramov]

Yeah I actually ended up close to your approach (nothing too fancy) but it can be made a lot more concise and legible by adding some machinery.

[Dan Abramov]

Alright, here goes! https://github.com/teorth/analysis/pull/360

[Rado Kirov]

Nice! You used the split to n disjoint sets approach and the specialized card lemma for this. That is cleaner that the explicit Permutations n + 1 ~ Fin (n + 1) \x Permutations n bijection I used.