seminormFromConst_bddBelow — Mathlib

English

The range of the sequence seminormFromConst_seq(x) is bounded below; in particular, there exists a real lower bound (namely 0) for all its terms.

Русский

Образ последовательности $\operatorname{seminormFromConstSeq}(x)$ ограничен снизу; в частности, 0 служит нижним пределом для всех её членов.

LaTeX

$$BddBelow( Set.range( seminormFromConst_seq c f x))$$

Lean4

/-- The image of `seminormFromConst_seq c f x` is bounded below by zero. -/
theorem seminormFromConst_bddBelow (x : R) : BddBelow (Set.range (seminormFromConst_seq c f x)) :=
  by
  use 0
  rintro r ⟨n, rfl⟩
  exact seminormFromConst_seq_nonneg c f x n

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