lipschitzWith_ofFun_iff — Mathlib

English

LipschitzWith K (x ↦ ofFun (f x)) holds iff for all c, LipschitzWith K (x ↦ f x c).

Русский

LipschitzWith K (x ↦ ofFun (f x)) эквивалентно ∀ c, LipschitzWith K (x ↦ f x c).

LaTeX

$$\text{LipschitzWith}(K, x \mapsto \mathrm{ofFun}(f x)) \iff \forall c, \text{LipschitzWith}(K, x \mapsto f(x)c)$$

Lean4

theorem lipschitzWith_ofFun_iff {f : γ → α → β} {K : ℝ≥0} :
    LipschitzWith K (fun x ↦ ofFun (f x)) ↔ ∀ c, LipschitzWith K (f · c) :=
  lipschitzWith_iff

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