smoothingSeminormSeq_bddBelow — Mathlib

English

For any x, the smoothingSeminormSeq μ x is bounded below by 0; equivalently, the range is contained in [0, ∞).

Русский

Для любого x последовательность smoothingSeminormSeq μ x ограничена снизу нулём; иначе говоря, значения лежат в [0, ∞).

LaTeX

$$BddBelow (Set.range (fun n => μ (x^n)^{1/n}))$$

Lean4

/-- `smoothingSeminormSeq` is bounded below (by zero). -/
theorem smoothingSeminormSeq_bddBelow (x : R) : BddBelow (Set.range fun n : ℕ+ => μ (x ^ (n : ℕ)) ^ (1 / (n : ℝ))) :=
  ⟨0, zero_mem_lowerBounds_smoothingSeminormSeq_range μ x⟩

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