Mathlib Map

Theorems · Theorem · commutative algebra

smoothingFun_nonneg

∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R), μ 1 ≤ 1 → ∀ (x : R), 0 ≤ smoothingFun μ x

If μ 1 ≤ 1, then smoothingFun μ x is nonnegative.

Defined in
Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
Cited by
1 results in Mathlib
Foundations
Depth 208 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CommRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

isNonarchimedean_smoothingFun · cited by 1isNonarchimedean_smoothin…DFunLike.coe · cited by 62936DFunLike.coeReal · cited by 25697RealCommRing · cited by 17173CommRingReal.rpow_nonneg · cited by 111Real.rpow_nonnegNonnegHomClass.apply_nonneg · cited by 79NonnegHomClass.apply_nonn…RingSeminorm · cited by 58RingSeminormge_of_tendsto · cited by 29ge_of_tendstosmoothingFun · cited by 13smoothingFuntendsto_smoothingFun_of_map_one_le_one · cited by 7tendsto_smoothingFun_of_m…smoothingFun_nonnegCITED BYCITES

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.