fst_map_prodMk

Mathlib.MeasureTheory.Measure.Prod

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.fst_map_prodMk

← MathLib Explorer

English

If Y is measurable, then (μ.map (a ↦ (X a, Y a))).fst = μ.map X.

Русский

Если Y измерима, то (μ.map (a ↦ (X a, Y a))).fst = μ.map X.

LaTeX

$$$$ (\\mu.\\mathrm{map} (\\lambda a, (X a, Y a))).fst = \\mu.\\mathrm{map} X $$$$

Lean4

theorem fst_map_prodMk {X : α → β} {Y : α → γ} {μ : Measure α} (hY : Measurable Y) :
    (μ.map fun a => (X a, Y a)).fst = μ.map X :=
  fst_map_prodMk₀ hY.aemeasurable

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

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

Разделы

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

Аффилиация

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