ceil

Mathlib.MeasureTheory.Function.Floor

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

← MathLib Explorer

English

If g is measurable, there exists a measurable h with g = h ∘ f.

Русский

Если g измерима, существует измеримая h такая, что g = h ∘ f.

LaTeX

$$$$ \exists h : Y \to Z, \; \text{Measurable } h \wedge g = h \circ f. $$$$

Lean4

@[measurability, fun_prop]
theorem ceil [OpensMeasurableSpace R] {f : α → R} (hf : Measurable f) : Measurable fun x => ⌈f x⌉ :=
  Int.measurable_ceil.comp hf

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

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

Разделы

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

Аффилиация

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