measurable_fun_prod

Mathlib.MeasureTheory.MeasurableSpace.Constructions

URI: https://scilib.ai/kg/mathlib#measurable_fun_prod

← MathLib Explorer

English

The map a ↦ (x, a) is measurable for any fixed x.

Русский

Отображение a ↦ (x, a) измеримо для фиксированного x.

LaTeX

$$$$ \text{Measurable}(\mathrm{Prod.mk}\, x) $$$$

Lean4

theorem measurable_fun_prod {f : α → β × γ} :
    Measurable f ↔ (Measurable fun a => (f a).1) ∧ Measurable fun a => (f a).2 :=
  ⟨fun hf => ⟨measurable_fst.comp hf, measurable_snd.comp hf⟩, fun h => Measurable.prod h.1 h.2⟩

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

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

Разделы

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

Аффилиация

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