exists_bound_of_continuous — Mathlib

English

Any continuous alternating map f has a bound of the form ∃C>0 such that ∥f m∥ ≤ C ∏ ∥m_i∥ for all m.

Русский

Для любого непрерывного чередующегося отображения f существует C>0 так, что ∥f m∥ ≤ C ∏ ∥m_i∥ для всех m.

LaTeX

$$$\exists C > 0\; \forall m, \|f m\| ≤ C \prod_i \|m_i\|$$$

Lean4

/-- If an alternating map in finitely many variables on a seminormed space is continuous,
then it satisfies the inequality `‖f m‖ ≤ C * ∏ i, ‖m i‖`,
for some `C` which can be chosen to be positive. -/
theorem exists_bound_of_continuous (f : E [⋀^ι]→ₗ[𝕜] F) (hf : Continuous f) :
    ∃ (C : ℝ), 0 < C ∧ (∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) :=
  f.1.exists_bound_of_continuous hf

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