measurable_swap_iff

Mathlib.MeasureTheory.MeasurableSpace.Constructions

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

← MathLib Explorer

English

Measurable (f ∘ Prod.swap) iff Measurable f.

Русский

Measurable (f ∘ Prod.swap) эквивалентно Measurable f.

LaTeX

$$$$ \text{Measurable}(f \circ \mathrm{Prod.swap}) \iff \text{Measurable}(f) $$$$

Lean4

theorem measurable_swap_iff {_ : MeasurableSpace γ} {f : α × β → γ} : Measurable (f ∘ Prod.swap) ↔ Measurable f :=
  ⟨fun hf => hf.comp measurable_swap, fun hf => hf.comp measurable_swap⟩

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

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

Разделы

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

Аффилиация

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