lipschitz_with_lipschitz_const_mul

English

For any β with LipschitzMul, the map (p,q) ↦ p.1 · p.2 is Lipschitz with constant Cβ.

Русский

Для любых β с LipschitzMul отображение (p,q) ↦ p₁p₂ Lipschitz с константой Cβ.

LaTeX

$$$\\forall p,q \\in β×β,\\ dist(p_1p_2, q_1q_2) \\le C_β \\cdot dist(p,q).$$$

Lean4

@[to_additive]
theorem lipschitz_with_lipschitz_const_mul :
    ∀ p q : β × β, dist (p.1 * p.2) (q.1 * q.2) ≤ LipschitzMul.C β * dist p q :=
  by
  rw [← lipschitzWith_iff_dist_le_mul]
  exact lipschitzWith_lipschitz_const_mul_edist

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