English
There exists a measurable equivalence between (Π i∈Iic a, X_i) × (Π i∈Ioc a b, X_i) and Π i∈Iic b, X_i when a ≤ b; the forward map is the gluing IicProdIoc and the inverse uses the natural splitting into left and right components.
Русский
Если a ≤ b, то между произведениями по левой и правой частям и линеаризацией по Iic b существует измеримое эквивалентное отображение, частично задающееся через IicProdIoc.
LaTeX
$$$\text{IicProdIoc}: ((\Pi i∈Iic a, X_i) × (\Pi i∈Ioc a b, X_i)) \simeq^\mathrm{meas} (\Pi i∈Iic b, X_i)$$$
Lean4
/-- Gluing `Iic a` and `Ioc a b` into `Iic b`. This version requires `a ≤ b` to get a measurable
equivalence. -/
def IicProdIoc {a b : ι} (hab : a ≤ b) : ((Π i : Iic a, X i) × (Π i : Ioc a b, X i)) ≃ᵐ Π i : Iic b, X i
where
toFun x i := if h : i ≤ a then x.1 ⟨i, mem_Iic.2 h⟩ else x.2 ⟨i, mem_Ioc.2 ⟨not_le.1 h, mem_Iic.1 i.2⟩⟩
invFun x := ⟨fun i ↦ x ⟨i.1, Iic_subset_Iic.2 hab i.2⟩, fun i ↦ x ⟨i.1, Ioc_subset_Iic_self i.2⟩⟩
left_inv := fun x ↦ by
ext i
· simp [mem_Iic.1 i.2]
· simp [not_le.2 (mem_Ioc.1 i.2).1]
right_inv := fun x ↦ funext fun i ↦ by by_cases hi : i.1 ≤ a <;> simp [hi]
measurable_toFun := by
refine measurable_pi_lambda _ (fun x ↦ ?_)
by_cases h : x ≤ a
· simpa [h] using measurable_fst.eval
· simpa [h] using measurable_snd.eval
measurable_invFun := by dsimp; fun_prop
