mkContinuous₂_apply — Mathlib

English

A refined bound shows that the mkContinuous₂ construction yields a controlled norm when applied to a bound C and a base input x.

Русский

Уточненное ограничение для конструктивной нормировки mkContinuous₂ дает управляемую норму при заданной константе C и входном x.

LaTeX

$$$ \| (f x).mkContinuous (C\|x\|) hC x \| \le \max\{C,0\} \|x\| $$$

Lean4

@[simp]
theorem mkContinuous₂_apply (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) {C : ℝ} (hC : ∀ x y, ‖f x y‖ ≤ C * ‖x‖ * ‖y‖) (x : E)
    (y : F) : f.mkContinuous₂ C hC x y = f x y :=
  rfl

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