bounds_nonempty — Mathlib

English

There exists a nonnegative constant C such that for all m, ∥f(m)∥ ≤ C ∏_i ∥m_i∥.

Русский

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

LaTeX

$$$$\\exists C \\ge 0\\;\\forall m,\\; \\|f m\\| \\le C \\prod_i \\|m_i\\|.$$$$

Lean4

theorem bounds_nonempty {f : ContinuousMultilinearMap 𝕜 E G} : ∃ c, c ∈ {c | 0 ≤ c ∧ ∀ m, ‖f m‖ ≤ c * ∏ i, ‖m i‖} :=
  let ⟨M, hMp, hMb⟩ := f.bound
  ⟨M, le_of_lt hMp, hMb⟩

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