smoothingFun_le_self — Mathlib

English

For all x, smoothingFun μ x ≤ μ x.

Русский

Для всех x выполняется smoothingFun μ x ≤ μ x.

LaTeX

$$$smoothingFun μ x ≤ μ x$$$

Lean4

/-- For all `x : R`, `smoothingFun μ x ≤ μ x`. -/
theorem smoothingFun_le_self (x : R) : smoothingFun μ x ≤ μ x :=
  by
  apply (smoothingFun_le μ x 1).trans
  rw [PNat.one_coe, pow_one, cast_one, div_one, rpow_one]
    /- In this section, we prove that if `μ` is nonarchimedean, then `smoothingFun μ` is
      nonarchimedean. -/

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