coe_mkContinuous — Mathlib

English

There exists a positive bound C such that ∥f m∥ ≤ C ∏ ∥m_i∥ for all m, for a continuous multilinear map f.

Русский

Существует положительная граница C, такая что ∥f m∥ ≤ C ∏ ∥m_i∥ для всех m, если f непрерывна.

LaTeX

$$∃ C > 0, ∀ m, ∥f m∥ ≤ C ∏ i ∥m_i∥$$

Lean4

@[simp]
theorem coe_mkContinuous (f : MultilinearMap 𝕜 E G) (C : ℝ) (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) :
    ⇑(f.mkContinuous C H) = f :=
  rfl

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