English
Gluing Iic a and Ioi a into the natural numbers ℕ yields a measurable equivalence between the product over Iic a and Ioi a and the product over ℕ.
Русский
Сшивка Iic a и Ioi a в ℕ задаёт измеримую эквивалентность между соответствующими произведениями и произведением по ℕ.
LaTeX
$$$((\Pi i∈Iic a, X_i) × (\Pi i∈Ioi a, X_i)) \simeq^{\mathrm{meas}} (\Pi n, X_n)$$$
Lean4
/-- Gluing `Iic a` and `Ioi a` into `ℕ`, version as a measurable equivalence
on dependent functions. -/
def IicProdIoi (a : ι) : ((Π i : Iic a, X i) × (Π i : Set.Ioi a, X i)) ≃ᵐ (Π n, X n)
where
toFun := fun x i ↦ if hi : i ≤ a then x.1 ⟨i, mem_Iic.2 hi⟩ else x.2 ⟨i, Set.mem_Ioi.2 (not_le.1 hi)⟩
invFun := fun x ↦ (fun i ↦ x i, fun i ↦ x i)
left_inv := fun x ↦ by
ext i
· simp [mem_Iic.1 i.2]
· simp [not_le.2 <| Set.mem_Ioi.1 i.2]
right_inv := fun x ↦ by simp
measurable_toFun := by
refine measurable_pi_lambda _ (fun i ↦ ?_)
by_cases hi : i ≤ a <;> simp only [Equiv.coe_fn_mk, hi, ↓reduceDIte]
· exact measurable_fst.eval
· exact measurable_snd.eval
measurable_invFun := Measurable.prodMk (measurable_restrict _) (Set.measurable_restrict _)