Relation between general cartesian product and prod

Stream: maths

[Esteban Martínez Vañó]

Hi everyone.

Is there a relation between the general cartesian product and the prod type?

For example, I have the following theorem:

theorem prod_limit  {X ι D: Type*} {π : ι → Type*} [DirectedSet D] [TopologicalSpace X] [T : (i : ι) → TopologicalSpace (π i)]
  (s: D → (i : ι) → π i) (x: (i : ι) → π i) : Limit s x ↔ ∀ (i: ι), Limit (fun (d: D) ↦ s d i) (x i)

(It doesn't matter for the question how Limit and DirectedSet are defined)

And I want to apply it to a net of the form s: D → X × Y. Is there a nice way to use the previous theorem to work with this case?

For example, is there a simple way of proving

theorem prod_limit'  {X Y D: Type*} [DirectedSet D] [TopologicalSpace X] [TopologicalSpace Y]
  (s: D → X × Y) (x: X × Y) : Limit s x ↔ Limit (fun (d: D) ↦ (s d).1) x.1 ∧ Limit (fun (d: D) ↦ (s d).2) x.2

using the previous theorem?

Thanks in advance for any help.

[Daniel Weber]

There's docs#Equiv.boolArrowEquivProd, and you can also define

import Mathlib

/-- The function type `((a : Bool) → bif a then β else α)` is equivalent to `α × β`. -/
@[simps]
def boolPiEquivProd (α) : ((a : Bool) → bif a then β else α) ≃ α × β where
  toFun f := (f false, f true)
  invFun p b := b.casesOn p.1 p.2
  left_inv _ := funext <| Bool.forall_bool.2 ⟨rfl, rfl⟩
  right_inv := fun _ => rfl

but there's nothing inherent

[Esteban Martínez Vañó]

Okay thanks.

Then I thinks it is easier to directly prove the second version and have both.