sup_apply

Mathlib.Analysis.Normed.Group.Seminorm

URI: https://scilib.ai/kg/mathlib#NonarchAddGroupSeminorm.sup_apply

English

For p, q ∈ NonarchAddGroupSeminorm E and x ∈ E, (p ⊔ q) x = p x ⊔ q x, i.e., the value at x is the maximum of the values.

Русский

Для p, q ∈ NonarchAddGroupSeminorm E и x ∈ E, (p ⊔ q) x = p x ⊔ q x, то есть значение в x равно максимуму значений.

LaTeX

$$$ (p \sqcup q) x = p x \sqcup q x $$$

Lean4

@[simp]
theorem sup_apply (x : E) : (p ⊔ q) x = p x ⊔ q x :=
  rfl

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

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

Разделы

Аффилиация

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