floor

Mathlib.MeasureTheory.Function.Floor

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

← MathLib Explorer

English

If f is measurable, then the floor of f is measurable: floor(f(x)) is a measurable function.

Русский

Если f измерима, то floor(f(x)) измерима.

LaTeX

$$$$ \text{Measurable }( \lambda x, \lfloor f(x) \rfloor ). $$$$

Lean4

@[measurability, fun_prop]
theorem floor [OpensMeasurableSpace R] {f : α → R} (hf : Measurable f) : Measurable fun x => ⌊f x⌋ :=
  Int.measurable_floor.comp hf

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

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

Разделы

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

Аффилиация

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