continuous_of_forall_lipschitzWith

English

If a γ → UniformOnFun α β 𝔖 has each coordinate Lipschitz on s, then the function γ → UniformOnFun α β 𝔖 is continuous.

Русский

Если каждая координата Lipschitz на s, то отображение γ → UniformOnFun α β 𝔖 непрерывно на s.

LaTeX

$$Continuous f$$

Lean4

/-- Let `f : γ → α →ᵤ[𝔖] β`. If for every `s ∈ 𝔖` and for every `c ∈ s`, the function
`fun x ↦ f x c` is Lipschitz (with Lipschitz constant depending on `s`), then `f` is continuous. -/
theorem continuous_of_forall_lipschitzWith {f : γ → α →ᵤ[𝔖] β} (K : Set α → ℝ≥0)
    (h : ∀ s ∈ 𝔖, ∀ c ∈ s, LipschitzWith (K s) (fun x ↦ toFun 𝔖 (f x) c)) : Continuous f :=
  by
  rw [UniformOnFun.continuous_rng_iff]
  refine fun s hs ↦ LipschitzWith.continuous (K := K s) ?_
  rw [UniformFun.lipschitzWith_iff]
  rintro ⟨y, hy⟩
  exact h s hs y hy

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