inf_apply

Mathlib.Analysis.Seminorm

URI: https://scilib.ai/kg/mathlib#Seminorm.inf_apply

English

The scalar action distributes over the infimum: r • (p ⊓ q) = (r • p) ⊓ (r • q).

Русский

Скалярное умножение распределяется над инфимумом: r • (p ⊓ q) = (r • p) ⊓ (r • q).

LaTeX

$$$r \cdot (p \inf q) = (r \cdot p) \inf (r \cdot q)$$$

Lean4

@[simp]
theorem inf_apply (p q : Seminorm 𝕜 E) (x : E) : (p ⊓ q) x = ⨅ u : E, p u + q (x - u) :=
  rfl

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

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

Разделы

Аффилиация

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