smoothingSeminorm_map_one_le_one — Mathlib

English

For hμ1 and hna, the smoothingSeminorm μ hμ1 hna satisfies smoothingSeminorm μ hμ1 hna 1 ≤ 1.

Русский

Для hμ1 и hna выполняется smoothingSeminorm μ hμ1 hna 1 ≤ 1.

LaTeX

$$smoothingSeminorm μ hμ1 hna 1 ≤ 1$$

Lean4

/-- If `μ 1 ≤ 1` and `μ` is nonarchimedean, then `smoothingSeminorm μ 1 ≤ 1`. -/
theorem smoothingSeminorm_map_one_le_one (hμ1 : μ 1 ≤ 1) (hna : IsNonarchimedean μ) :
    smoothingSeminorm μ hμ1 hna 1 ≤ 1 :=
  smoothingFun_one_le μ hμ1

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