sup'

Mathlib.MeasureTheory.Order.Lattice

URI: https://scilib.ai/kg/mathlib#AEMeasurable.sup'

← MathLib Explorer

English

If f and g are AEMeasurable, then x ↦ f(x) ⊔ g(x) is AEMeasurable.

Русский

Если f и g AEMeasurable, то x ↦ f(x) ⊔ g(x) является AEMeasurable.

LaTeX

$$$AEMeasurable(f,\mu) \Rightarrow AEMeasurable(g,\mu) \Rightarrow AEMeasurable\bigl(x \mapsto f(x) \sqcup g(x)\bigr)\mu$$$

Lean4

@[measurability]
theorem sup' (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : AEMeasurable (f ⊔ g) μ :=
  measurable_sup.comp_aemeasurable (hf.prodMk hg)

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

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

Разделы

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

Аффилиация

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