uniformContinuous_restrict_toFun — Mathlib

English

The restriction map from α →ᵤ[𝔖] β to (⋃₀ 𝔖) → β is uniformly continuous.

Русский

Ограничение отображает пространство 𝔖-конвергенций на объединение 𝔖 в пространство функций α → β равномерно непрерывно.

LaTeX

$$UniformContinuous((⋃₀ 𝔖).restrict ∘ toFun 𝔖).$$

Lean4

/-- The restriction map from `α →ᵤ[𝔖] β` to `⋃₀ 𝔖 → β` is uniformly continuous. -/
theorem uniformContinuous_restrict_toFun : UniformContinuous ((⋃₀ 𝔖).restrict ∘ toFun 𝔖 : (α →ᵤ[𝔖] β) → ⋃₀ 𝔖 → β) :=
  by
  rw [uniformContinuous_pi]
  intro ⟨x, hx⟩
  obtain ⟨s : Set α, hs : s ∈ 𝔖, hxs : x ∈ s⟩ := mem_sUnion.mpr hx
  exact uniformContinuous_eval_of_mem β 𝔖 hxs hs

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