piFinTwo — Mathlib

English

The space of functions from Fin(2) to a family α i is measurably equivalent to the product α0 × α1.

Русский

Место функций из Fin(2) в семействе α i измеримо эквивалентно произведению α0 × α1.

LaTeX

$$$ (\\forall i:\\mathrm{Fin}(2), \\alpha_i) \\simeq^m \\alpha_0 \\times \\alpha_1 $$$

Lean4

/-- The space `Π i : Fin 2, α i` is measurably equivalent to `α 0 × α 1`. -/
@[simps! -fullyApplied]
def piFinTwo (α : Fin 2 → Type*) [∀ i, MeasurableSpace (α i)] : (∀ i, α i) ≃ᵐ α 0 × α 1
    where
  toEquiv := piFinTwoEquiv α
  measurable_toFun := Measurable.prod (measurable_pi_apply _) (measurable_pi_apply _)
  measurable_invFun := measurable_pi_iff.2 <| Fin.forall_fin_two.2 ⟨measurable_fst, measurable_snd⟩

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