mul_bddBelow_range_add

Mathlib.Analysis.Normed.Group.Seminorm

URI: https://scilib.ai/kg/mathlib#GroupSeminorm.mul_bddBelow_range_add

← MathLib Explorer

English

Same as above with the explicit GroupSeminorm instance; p.comp (f g) ≤ p.comp f + p.comp g.

Русский

То же самое: p.comp (f g) ≤ p.comp f + p.comp g.

LaTeX

$$$p \comp (f g) \le p \comp f + p \comp g$$$

Lean4

@[to_additive]
theorem mul_bddBelow_range_add {p q : GroupSeminorm E} {x : E} : BddBelow (range fun y => p y + q (x / y)) :=
  ⟨0, by
    rintro _ ⟨x, rfl⟩
    dsimp
    positivity⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru