lipschitzWith_lipschitz_const_mul_edist

English

The map (p, q) ↦ p.1 · p.2 is Lipschitz with constant Cβ, i.e., dist(p₁p₂, q₁q₂) ≤ Cβ · dist((p₁,p₂), (q₁,q₂)).

Русский

Отображение \n( p, q ) ↦ p₁ p₂ липшицевско ограничено константой Cβ: dist(p₁p₂, q₁q₂) ≤ Cβ dist(p, q).

LaTeX

$$$\\operatorname{LipschitzWith}(C_β)\\big((p_1,p_2),(q_1,q_2)\\big).$$$

Lean4

@[to_additive]
theorem lipschitzWith_lipschitz_const_mul_edist [_i : LipschitzMul β] :
    LipschitzWith (LipschitzMul.C β) fun p : β × β => p.1 * p.2 :=
  Classical.choose_spec _i.lipschitz_mul

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