comp_mono

Mathlib.Analysis.Seminorm

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

English

Composing with the zero map yields the zero seminorm: p ∘ 0 = 0.

Русский

Составление с нулевым отображением даёт нулевую полунорму: p ∘ 0 = 0.

LaTeX

$$$ p \circ 0 = 0 $$$

Lean4

theorem comp_mono {p q : Seminorm 𝕜₂ E₂} (f : E →ₛₗ[σ₁₂] E₂) (hp : p ≤ q) : p.comp f ≤ q.comp f := fun _ => hp _

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

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

Разделы

Аффилиация

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