mkContinuousAlternating_norm_le_max

English

If f satisfies a growth condition ‖f m₁ m₂‖ ≤ (C*∏ ‖m₁ i‖) ∏ ‖m₂ i‖, then the norm of mkContinuousAlternating f C H is bounded by max(C,0).

Русский

Если отображение f удовлетворяет ограничению роста, то норма mkContinuousAlternating f C H не превосходит max(C,0).

LaTeX

$$$\\\\| mkContinuousAlternating f C H \\\\| \\\\le \\\\max(C, 0)$$$

Lean4

theorem mkContinuousAlternating_norm_le_max (f : E [⋀^ι]→ₗ[𝕜] (F [⋀^ι']→ₗ[𝕜] G)) {C : ℝ}
    (H : ∀ m₁ m₂, ‖f m₁ m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖) : ‖mkContinuousAlternating f C H‖ ≤ max C 0 :=
  by
  dsimp only [mkContinuousAlternating]
  exact mkContinuous_norm_le _ (le_max_right _ _) _

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