abs_self_eq_nnrealPart_add_nnrealPart_neg

English

For every real-valued bounded continuous f, the absolute value at each point equals the sum of its positive and negative parts: |f(x)| = (f(x))^+ + ((-f(x))^+).

Русский

У любого f выполняется |f(x)| = f(x)^+ + (-f(x))^+ для всех x.

LaTeX

$$$$\forall f:\, \alpha \to^b \mathbb{R},\; |f(x)| = (f(x))^+ + ((-f(x))^+).$$$$

Lean4

/-- Express the absolute value of a bounded continuous function in terms of its
positive and negative parts. -/
theorem abs_self_eq_nnrealPart_add_nnrealPart_neg (f : α →ᵇ ℝ) :
    abs ∘ ⇑f = (↑) ∘ f.nnrealPart + (↑) ∘ (-f).nnrealPart :=
  by
  funext x
  dsimp
  simp only [max_zero_add_max_neg_zero_eq_abs_self]

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