English
For n ∈ N and i ∈ Fin(n+1), there is a measurable equivalence between (∀ j, α j) and α i × ∀ j, α (i.succAbove j).
Русский
Для каждого n и i∈Fin(n+1) существует измеримая эквивалентность между (∀ j, α j) и α i × ∀ j, α (i.succAbove j).
LaTeX
$$$ (\\forall j:\\mathrm{Fin}(n), \\alpha_j) \\simeq^m \\alpha_i \\times \\forall j:\\mathrm{Fin}(n), \\alpha( i .\\mathrm{succAbove} j) $$$
Lean4
/-- Measurable equivalence between `Π j : Fin (n + 1), α j` and
`α i × Π j : Fin n, α (Fin.succAbove i j)`.
Measurable version of `Fin.insertNthEquiv`. -/
@[simps! -fullyApplied]
def piFinSuccAbove {n : ℕ} (α : Fin (n + 1) → Type*) [∀ i, MeasurableSpace (α i)] (i : Fin (n + 1)) :
(∀ j, α j) ≃ᵐ α i × ∀ j, α (i.succAbove j)
where
toEquiv := (Fin.insertNthEquiv α i).symm
measurable_toFun := (measurable_pi_apply i).prodMk <| measurable_pi_iff.2 fun _ => measurable_pi_apply _
measurable_invFun :=
measurable_pi_iff.2 <|
i.forall_iff_succAbove.2
⟨by simp [measurable_fst], fun j => by simpa using (measurable_pi_apply _).comp measurable_snd⟩
