add_bddBelow_range_add — Mathlib

English

For p, q ∈ NonarchAddGroupSeminorm E and for x ∈ E, the range of y ↦ p(y) + q(x − y) is bounded below (by 0).

Русский

Для p, q ∈ NonarchAddGroupSeminorm E и для x ∈ E диапазон y ↦ p(y) + q(x − y) ограничен снизу (нулём).

LaTeX

$$$ BddBelow\left( \operatorname{range} \bigl( y \mapsto p(y) + q(x-y) \bigr) \right) $ with lower bound 0, i.e., ∀y, p(y) + q(x-y) ≥ 0.$$

Lean4

theorem add_bddBelow_range_add {p q : NonarchAddGroupSeminorm E} {x : E} : BddBelow (range fun y => p y + q (x - y)) :=
  ⟨0, by
    rintro _ ⟨x, rfl⟩
    dsimp
    positivity⟩

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