comp — Mathlib

English

The family of seminorms obtained by composing each seminorm in q with a fixed linear map f is again a seminorm family on E, i.e., q.comp f is a SeminormFamily 𝕜 E ι given by i ↦ (q i).comp f.

Русский

Семейство семинорм, полученное путём композиции каждой нормой из q с фиксированным линейным отображением f, снова образует семейство семинорм на E: q.comp f.

LaTeX

$$$ SeminormFamily.comp (q) (f) : SeminormFamily 𝕜 E ι $$$

Lean4

/-- The family of seminorms obtained by composing each seminorm by a linear map. -/
def comp (q : SeminormFamily 𝕜₂ F ι) (f : E →ₛₗ[σ₁₂] F) : SeminormFamily 𝕜 E ι := fun i => (q i).comp f

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