uniformContinuous_restrict — Mathlib

English

For f ∈ α →ᵤ[𝔖] β with 𝔖 nonempty and directed, the neighborhoods 𝓝 f have a basis consisting of sets of the form {g | ∀ x ∈ S, (f x, g x) ∈ V} with S ∈ 𝔖 and V a basis element of 𝓤 β.

Русский

Для f ∈ α →ᵤ[𝔖] β при 𝔖 непустом и направленном, окрестности 𝓝 f имеют базис в виде множеств {g | ∀ x∈S, (f x, g x) ∈ V} с S∈𝔖 и V базиса 𝓤 β.

LaTeX

$$$\text{nhds } f = \bigwedge_{S\in 𝔖} \bigwedge_{V∈𝓤 β} \mathcal P\{ g : ∀ x∈S, (f x, g x) ∈ V\}.$$$

Lean4

/-- If `S ∈ 𝔖`, then the restriction to `S` is a uniformly continuous map from `α →ᵤ[𝔖] β` to
`↥S →ᵤ β`. -/
protected theorem uniformContinuous_restrict (h : s ∈ 𝔖) :
    UniformContinuous (UniformFun.ofFun ∘ (s.restrict : (α → β) → s → β) ∘ toFun 𝔖) :=
  by
  change _ ≤ _
  simp only [UniformOnFun.uniformSpace, map_le_iff_le_comap, iInf_uniformity]
  exact iInf₂_le s h

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