compCLMOfAntilipschitz_apply — Mathlib

English

For any K, g with temperate growth and antilipschitzWith K g, and f ∈ 𝓢(E, F), the equality compCLMOfAntilipschitz 𝕜 hg h'g f = f ∘ g holds.

Русский

Для любого K, g с темпериированным ростом и антиплохостью с константой K, и f ∈ 𝓢(E,F), выполняется равенство compCLMOfAntilipschitz 𝕜 hg h'g f = f ∘ g.

LaTeX

$$$compCLMOfAntilipschitz 𝕜 hg h'g\ f = f \circ g$$$

Lean4

@[simp]
theorem compCLMOfAntilipschitz_apply {K : ℝ≥0} {g : D → E} (hg : g.HasTemperateGrowth) (h'g : AntilipschitzWith K g)
    (f : 𝓢(E, F)) : compCLMOfAntilipschitz 𝕜 hg h'g f = f ∘ g :=
  rfl

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