bddBelow_range_add — Mathlib

English

There exists a lattice structure on seminorms: the infimum of two seminorms is defined by the convolution (p ⊓ q)(x) = inf_u (p(u) + q(x-u)).

Русский

Существует решетка над семинормами: инфимум двух семинорм задаётся свёрткой (p ⊓ q)(x) = inf_u (p(u) + q(x-u)).

LaTeX

$$$(p \inf q)(x) = \inf_{u \in E} \left( p(u) + q(x-u) \right)$$$

Lean4

/-- Auxiliary lemma to show that the infimum of seminorms is well-defined. -/
theorem bddBelow_range_add : BddBelow (range fun u => p u + q (x - u)) :=
  ⟨0, by
    rintro _ ⟨x, rfl⟩
    dsimp; positivity⟩

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