continuous_posPart — Mathlib

English

The map sending an Lp-function to its positive part is continuous (Lipschitz with constant 1) on the Lp-space, provided p≥1.

Русский

Отображение f→posPart f непрерывно на Lp-пространстве при p≥1 (Lipschitz с константой 1).

LaTeX

$$$\text{Continuous}\\ f \mapsto \text{posPart}(f)\;\text{on } L^p.$$

Lean4

theorem continuous_posPart [Fact (1 ≤ p)] : Continuous fun f : Lp ℝ p μ => posPart f :=
  LipschitzWith.continuous_compLp _ _

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