smoothingFun_nonneg — Mathlib

English

If μ(1) ≤ 1, then smoothingFun μ x ≥ 0 for all x.

Русский

Если μ(1) ≤ 1, то smoothingFun μ x ≥ 0 для всех x.

LaTeX

$$$0 \le smoothingFun μ x$ for all x$$

Lean4

/-- If `μ 1 ≤ 1`, then `smoothingFun μ x` is nonnegative. -/
theorem smoothingFun_nonneg (hμ1 : μ 1 ≤ 1) (x : R) : 0 ≤ smoothingFun μ x :=
  by
  apply ge_of_tendsto (tendsto_smoothingFun_of_map_one_le_one μ hμ1 x)
  simpa [eventually_atTop, ge_iff_le] using ⟨1, fun _ _ ↦ rpow_nonneg (apply_nonneg μ _) _⟩

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