measurable

Mathlib.MeasureTheory.MeasurableSpace.Embedding

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

English

A measurable equivalence is measurable as a function.

Русский

Измеримое эквивалентное отображение является измеримым как функция.

LaTeX

$$$$ \text{MeasurableEquiv.measurable }(e) : \text{Measurable}(e : \alpha \to \beta). $$$$

Lean4

@[measurability, fun_prop]
protected theorem measurable (e : α ≃ᵐ β) : Measurable (e : α → β) :=
  e.measurable_toFun

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

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

Разделы

Аффилиация

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