measurable

Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

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

English

A continuous map f: α → γ is measurable.

Русский

Непрерывная карта f: α → γ измерима.

LaTeX

$$$\\mathrm{Measurable}(f)$ for $f: C(\\alpha,\\gamma)$ with underlying function.$$

Lean4

@[measurability]
theorem measurable (f : C(α, γ)) : Measurable f :=
  f.continuous.measurable

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

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

Разделы

Аффилиация

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