zero_comp

Mathlib.Analysis.Seminorm

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

English

The seminorm of a sum of maps is bounded by the sum of their seminorms: p ∘ (f + g) ≤ p ∘ f + p ∘ g.

Русский

Полунормa суммы отображений не превышает сумму их полунорм: p ∘ (f + g) ≤ p ∘ f + p ∘ g.

LaTeX

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

Lean4

@[simp]
theorem zero_comp (f : E →ₛₗ[σ₁₂] E₂) : (0 : Seminorm 𝕜₂ E₂).comp f = 0 :=
  ext fun _ => rfl

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

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

Разделы

Аффилиация

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