bounds_bddBelow — Mathlib

English

The set of admissible bounds for f is bounded below; in particular 0 is a lower bound.

Русский

Множество допустимых границ для f ограничено снизу; в частности 0 является нижней гранью.

LaTeX

$$$$\\text{BddBelow}\\;\\{c \\;|\\; 0 \\le c \\wedge \\forall m, \\|f m\\| \\le c \\prod_i \\|m_i\\|\\}.$$$

Lean4

theorem bounds_bddBelow {f : ContinuousMultilinearMap 𝕜 E G} : BddBelow {c | 0 ≤ c ∧ ∀ m, ‖f m‖ ≤ c * ∏ i, ‖m i‖} :=
  ⟨0, fun _ ⟨hn, _⟩ => hn⟩

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