Struggling to understand SetTheory.Set.tuple/iProd

Stream: Analysis I

[Dan Abramov]

In the book, we have:

Screenshot 2025-08-04 at 19.42.51.png

In code, we have:

/-- Definition 3.5.6 -/
abbrev SetTheory.Set.tuple {I:Set} {X: I → Set} (a: ∀ i, X i) : Object :=
  ((fun i ↦ ⟨ a i, by rw [mem_iUnion]; use i; exact (a i).property ⟩):I → iUnion I X)

/-- Definition 3.5.6 -/
abbrev SetTheory.Set.iProd {I: Set} (X: I → Set) : Set :=
  ((iUnion I X)^I).specify (fun t ↦ ∃ a : ∀ i, X i, t = tuple a)

I struggle with the connection here. In fact I find it difficult to see why this defines a tuple, or how it relates to OrderedPair (or even Lean tuples) from earlier.

I can guess that it's a more general notion but I wonder if there's some way it could've been explained with a few examples. I managed to construct this example with Claude's help but not sure it's actually helpful:

open Classical in
noncomputable example (A B : Set) (a : A) (b : B) : Object :=
  let I := ({0, 1} : Set)
  let X := fun (i: I) => if i.val = (0 : Object) then A else B
  let a : (i: I) → X i := fun (i: I) =>
    if h : i.val = (0 : Object) then
      ⟨a, by simp [X, h]; use a.property⟩
    else
      ⟨b, by simp [X, h]; use b.property⟩
  tuple a

I'm also noticing the definition looks a lot like 8.4.1:

Screenshot 2025-08-04 at 19.42.31.png

Did we, in a sense, jump further in the text? Although Section_8_4 also has its own definition:

/-- Definition 8.4.1 (Infinite Cartesian products).  We will avoid using this definition in favor
of the Mathlib form `∀ α, X α` which we will shortly show is equivalent to (or more precisely,
generalizes) this one.

Because Lean does not allow unrestricted unions of types, we cheat slightly here by assuming all the
`X α` are sets in a common universe `U`.  Note that the Mathlib definition does not have this
restriction. -/
abbrev CartesianProduct {I U: Type} (X : I → Set U) := { x : I → ⋃ α, X α // ∀ α, ↑(x α) ∈ X α }

To sum up, I feel a bit lost and I would've appreciated more connective tissue or comments around where tuple and iProd get introduced.

[Terence Tao]

Exercise 3.5.10 is intended to help connect this concept with the previous cartesian products. Definition 8.4.1 would correspond to the special case when the indexing set I is what is called Fin n in the next section, but it would be somewhat out of place to bring in the Fin API here to this section as we have no other use for it.

The API around the tuple and iProd concepts (i.e., mem_iProd, mem_iProd, tuple_mem_iProd, and tuple_inj are more important than the specific definitions of tuple and iProd themselves, and hopefully these can be seen to correspond to various counterparts in Definition 8.4.1.

[Terence Tao]

Added some comments to clarify, and also changed a to x to align closer to the text notation.