IicProdIoi — Mathlib

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 _)

Похожие утверждения