abs_truncation_le_abs_self — Mathlib

English

For every f,A,x, the absolute value of truncation is bounded by the absolute value of f:

Русский

Для любых f, A, x выполняется неравенство: |truncation(f,A)(x)| ≤ |f(x)|.

LaTeX

$$$|\operatorname{truncation}(f,A)(x)| \le |f(x)|$$$

Lean4

theorem abs_truncation_le_abs_self (f : α → ℝ) (A : ℝ) (x : α) : |truncation f A x| ≤ |f x| :=
  by
  simp only [truncation, indicator, id, Function.comp_apply]
  split_ifs
  · exact le_rfl
  · simp [abs_nonneg]

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