abs_truncation_le_bound — Mathlib

English

The absolute value of the truncation is bounded by the absolute value of A.

Русский

Модуль усечения не превышает модуль самой константы A.

LaTeX

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

Lean4

theorem abs_truncation_le_bound (f : α → ℝ) (A : ℝ) (x : α) : |truncation f A x| ≤ |A| :=
  by
  simp only [truncation, Set.indicator, id, Function.comp_apply]
  split_ifs with h
  · exact abs_le_abs h.2 (neg_le.2 h.1.le)
  · simp [abs_nonneg]

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