mkContinuousAlternating_norm_le — Mathlib

English

Under the same hypothesis as mkContinuousAlternating_norm_le_max but with a general C, we have ‖mkContinuousAlternating f C H‖ ≤ C when 0 ≤ C.

Русский

При тех же предположениях, но без ограничения на максимум, нормa равна не более C при неотрицательности C.

LaTeX

$$$\\\\| mkContinuousAlternating f C H \\\\| \\\\le C \\,\\;\\text{if } C \\ge 0$$$

Lean4

theorem mkContinuousAlternating_norm_le (f : E [⋀^ι]→ₗ[𝕜] (F [⋀^ι']→ₗ[𝕜] G)) {C : ℝ} (hC : 0 ≤ C)
    (H : ∀ m₁ m₂, ‖f m₁ m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖) : ‖mkContinuousAlternating f C H‖ ≤ C :=
  (mkContinuousAlternating_norm_le_max f H).trans_eq (max_eq_left hC)

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