of_uncurry_left

Mathlib.MeasureTheory.MeasurableSpace.Constructions

URI: https://scilib.ai/kg/mathlib#Measurable.of_uncurry_left

English

Given measurable f,g, the map a ↦ (f a, g a) is measurable.

Русский

Если f и g измеримы, отображение a ↦ (f(a), g(a)) измеримо.

LaTeX

$$$$ \text{Measurable}(a \mapsto (f a, g a)) $$$$

Lean4

theorem of_uncurry_left {f : α → β → γ} (hf : Measurable (uncurry f)) {x : α} : Measurable (f x) :=
  hf.comp measurable_prodMk_left

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

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

Разделы

Аффилиация

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