max — Mathlib

English

If f and g are measurable functions from δ to α, then the function a ↦ max(f(a), g(a)) is measurable.

Русский

Если f и g — измеримые функции, то функция a ↦ max(f(a), g(a)) измерима.

LaTeX

$$$\text{Measurable}(f) \land \text{Measurable}(g) \Rightarrow \text{Measurable}(\lambda a. \max\{f(a), g(a)\})$$$

Lean4

@[measurability, fun_prop]
theorem max {f g : δ → α} (hf : Measurable f) (hg : Measurable g) : Measurable fun a => max (f a) (g a) := by
  simpa only [max_def'] using hf.piecewise (measurableSet_le hg hf) hg

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