const_sup — Mathlib

English

For any measurable f, the map x ↦ c ⊔ f(x) is measurable for any constant c.

Русский

Для любой измеримой функции f отображение x ⇢ c ⊔ f(x) измеримо для любого константного c.

LaTeX

$$$(\operatorname{Measurable} f) \Rightarrow \forall c, \operatorname{Measurable}(x \mapsto c \sqcup f(x))$$$

Lean4

@[measurability]
theorem const_sup (hf : Measurable f) (c : M) : Measurable fun x => c ⊔ f x :=
  (measurable_const_sup c).comp hf

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