English
Identify a+1 with the interval Ioc(a, a+1) as a measurable equivalence between the singleton type X(a+1) and the dependent product over Ioc(a, a+1).
Русский
Идентифицировать a+1 с Ioc(a, a+1) как измеримую эквивалентность между X(a+1) и произведением по Ioc(a, a+1).
LaTeX
$$$X(a+1) \simeq^{\mathrm{meas}} \prod_{i\in Ioc(a,a+1)} X_i$$$
Lean4
/-- Identifying `{a + 1}` with `Ioc a (a + 1)`, as a measurable equiv on dependent functions. -/
def piSingleton (a : ℕ) : X (a + 1) ≃ᵐ Π i : Ioc a (a + 1), X i
where
toFun x i := (Nat.mem_Ioc_succ.1 i.2).symm ▸ x
invFun x := x ⟨a + 1, right_mem_Ioc.2 a.lt_succ_self⟩
left_inv := fun x ↦ by simp
right_inv := fun x ↦ funext fun i ↦ by cases Nat.mem_Ioc_succ' i; rfl
measurable_toFun := by
simp_rw [eqRec_eq_cast]
refine measurable_pi_lambda _ (fun i ↦ (MeasurableEquiv.cast _ ?_).measurable)
cases Nat.mem_Ioc_succ' i; rfl
measurable_invFun := measurable_pi_apply _
