piMeasurableEquivTProd

Mathlib.MeasureTheory.MeasurableSpace.Embedding

URI: https://scilib.ai/kg/mathlib#MeasurableEquiv.piMeasurableEquivTProd

Lean4

/-- Pi-types are measurably equivalent to iterated products. -/
@[simps! -fullyApplied]
def piMeasurableEquivTProd [DecidableEq δ'] {l : List δ'} (hnd : l.Nodup) (h : ∀ i, i ∈ l) :
    (∀ i, π i) ≃ᵐ List.TProd π l where
  toEquiv := List.TProd.piEquivTProd hnd h
  measurable_toFun := measurable_tProd_mk l
  measurable_invFun := measurable_tProd_elim' h

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru