lipschitzExtensionConstant_pos — Mathlib

English

There exists a bound C depending on E' such that for all Lipschitz data the extension constant multiplies the Lipschitz constant.

Русский

Существует предел C, зависящий от E', такой что для всех данных Lip f расширение даёт константу C·K.

LaTeX

$$$ \exists C>0,\forall M\ge0,\text{ if } \|u(v_i)\|\le M \Rightarrow \|u\| \le C \cdot M $$$

Lean4

theorem lipschitzExtensionConstant_pos (E' : Type*) [NormedAddCommGroup E'] [NormedSpace ℝ E']
    [FiniteDimensional ℝ E'] : 0 < lipschitzExtensionConstant E' :=
  by
  rw [lipschitzExtensionConstant]
  exact zero_lt_one.trans_le (le_max_right _ _)

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