English
There is a measurable equivalence between function spaces (α1 → β1) and (α2 → β2) induced by a base equivalence hα : α1 ≃ α2 and a measurable equivalence hβ : β1 ≃ᵐ β2.
Русский
Существует измеримая эквивалентность между пространствами функций (α1 → β1) и (α2 → β2), индуцируемая базовой эквивалентностью hα : α1 ≃ α2 и измеримой эквиваленцией hβ : β1 ≃ᵐ β2.
LaTeX
$$$ (\\alpha_1 \\to \\beta_1) \\equiv^m (\\alpha_2 \\to \\beta_2) $$$
Lean4
/-- The measurable equivalence `(α₁ → β₁) ≃ᵐ (α₂ → β₂)` induced by `α₁ ≃ α₂` and `β₁ ≃ᵐ β₂`. -/
def arrowCongr' {α₁ β₁ α₂ β₂ : Type*} [MeasurableSpace β₁] [MeasurableSpace β₂] (hα : α₁ ≃ α₂) (hβ : β₁ ≃ᵐ β₂) :
(α₁ → β₁) ≃ᵐ (α₂ → β₂) where
__ := Equiv.arrowCongr' hα hβ
measurable_toFun _
h := by exact MeasurableSet.preimage h <| measurable_pi_iff.mpr fun _ ↦ hβ.measurable.comp' (measurable_pi_apply _)
measurable_invFun _
h := by
exact MeasurableSet.preimage h <| measurable_pi_iff.mpr fun _ ↦ hβ.symm.measurable.comp' (measurable_pi_apply _)
