pullback — Mathlib

English

The composition with the sum of two maps is bounded by the sum of the compositions: p ∘ (f + g) ≤ p ∘ f + p ∘ g.

Русский

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

LaTeX

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

Lean4

/-- The composition as an `AddMonoidHom`. -/
@[simps]
def pullback (f : E →ₛₗ[σ₁₂] E₂) : Seminorm 𝕜₂ E₂ →+ Seminorm 𝕜 E
    where
  toFun := fun p => p.comp f
  map_zero' := zero_comp f
  map_add' := fun p q => add_comp p q f

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