coeFn_star — Mathlib

English

The a.e. equality between the star of an Lp-class representative and the pointwise star holds: coeFn_star.

Русский

Пошаговая эквивалентность: почти всюду star функции совпадает с точечным star соответствующего представителя.

LaTeX

$$$(\star f) =^{\mathrm{ae}} \star f$ a.e.$$

Lean4

theorem coeFn_star {p : ℝ≥0∞} (f : Lp R p μ) : (star f : Lp R p μ) =ᵐ[μ] star f :=
  (f : α →ₘ[μ] R).coeFn_star

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