of_finite

Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.StronglyMeasurable.of_finite

English

If α is finite, any f is strongly measurable.

Русский

Если α конечно, любая функция сильно измерима.

LaTeX

$$[Finite α] ⇒ StronglyMeasurable f$$

Lean4

@[deprecated StronglyMeasurable.of_discrete (since := "2025-04-09")]
theorem of_finite [Finite α] : StronglyMeasurable f :=
  .of_discrete

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

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

Разделы

Аффилиация

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