lipschitzMul — Mathlib

English

For a submonoid s of β, the structure inherits a LipschitzMul instance on the subtype.

Русский

Подмножество-субмоноид s наследует LipschitzMul на подтипе.

LaTeX

$$LipschitzMul s$$

Lean4

@[to_additive]
instance lipschitzMul (s : Submonoid β) : LipschitzMul s where
  lipschitz_mul :=
    ⟨LipschitzMul.C β, by
      rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩
      convert lipschitzWith_lipschitz_const_mul_edist ⟨(x₁ : β), x₂⟩ ⟨y₁, y₂⟩ using 1⟩

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