continuous_of_bound — Mathlib

English

If a bound ∥f m∥ ≤ C ∏ ∥m_i∥ holds, then f is continuous.

Русский

Если выполняется ограничение, то f непрерывно.

LaTeX

$$$\forall C,\; (\forall m, \|f m\| ≤ C \prod_i \|m_i\|) \Rightarrow \text{Continuous}(f)$$$

Lean4

/-- If an alternating map satisfies an inequality `‖f m‖ ≤ C * ∏ i, ‖m i‖`,
then it is continuous. -/
theorem continuous_of_bound (f : E [⋀^ι]→ₗ[𝕜] F) (C : ℝ) (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) : Continuous f :=
  f.toMultilinearMap.continuous_of_bound C H

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