bounds_bddBelow — Mathlib

English

The set of all admissible bounds c (0 ≤ c and ∀ m, ‖f m‖ ≤ c ∏ ‖m i‖) is bounded below.

Русский

Множество допустимых границ c (0 ≤ c и ∀ m, ‖f m‖ ≤ c ∏ ‖m i‖) ограничено снизу.

LaTeX

$$$$\exists \alpha \in \mathbb{R}, \; \alpha \le c \text{ for all } c \text{ with } 0 \le c \wedge \forall m,\|f m\| \le c \prod_i \|m_i\|.$$$$

Lean4

theorem bounds_bddBelow {f : E [⋀^ι]→L[𝕜] F} : BddBelow {c | 0 ≤ c ∧ ∀ m, ‖f m‖ ≤ c * ∏ i, ‖m i‖} :=
  ContinuousMultilinearMap.bounds_bddBelow

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