negPart_map_norm — Mathlib

English

The norm map of posPart for simple functions preserves the simple part: the map of the positive part under the norm equals the positive part itself.

Русский

Норма отображения posPart для простой функции сохраняет ее разложение на положительную часть.

LaTeX

$$$$ (posPart\, f).map\, \|\cdot\| = posPart\, f.$$$$

Lean4

theorem negPart_map_norm (f : α →ₛ ℝ) : (negPart f).map norm = negPart f := by rw [negPart]; exact posPart_map_norm _

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