coeFn_sup — Mathlib

English

The function representing the supremum of two Lp-elements equals almost everywhere the pointwise supremum of their representing functions.

Русский

Функция, соответствующая наибольшему из двух элементов Lp, почти везде равна точечному максимуму их образцов.

LaTeX

$$$\mathsf{ae}\,\mu\, (f\sqcup g) = (f|_\mathrm{coeFn}) \sqcup (g|_\mathrm{coeFn}).$$$

Lean4

theorem coeFn_sup (f g : Lp E p μ) : ⇑(f ⊔ g) =ᵐ[μ] ⇑f ⊔ ⇑g :=
  AEEqFun.coeFn_sup _ _

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