English
If MapsTo(f '' ·) 𝔗 𝔖, then the precomposition map g ↦ ofFun 𝔗 (toFun 𝔖 g ∘ f) is uniformly continuous.
Русский
Если выполняется MapsTo(f '' ·) 𝔗 𝔖, то отображение пред-композиции непрерывно по равномерности.
LaTeX
$$MapsTo (f '' ·) 𝔗 𝔖 → UniformContinuous (g : α →ᵤ[𝔖] β ⇒ ofFun 𝔗 (toFun 𝔖 g ∘ f)).$$
Lean4
/-- Let `f : γ → α`, `𝔖 : Set (Set α)`, `𝔗 : Set (Set γ)`, and assume that `∀ T ∈ 𝔗, f '' T ∈ 𝔖`.
Then, the function `(fun g ↦ g ∘ f) : (α →ᵤ[𝔖] β) → (γ →ᵤ[𝔗] β)` is uniformly continuous.
Note that one can easily see that assuming `∀ T ∈ 𝔗, ∃ S ∈ 𝔖, f '' T ⊆ S` would work too, but
we will get this for free when we prove that `𝒱(α, β, 𝔖, uβ) = 𝒱(α, β, 𝔖', uβ)` where `𝔖'` is the
***noncovering*** bornology generated by `𝔖`. -/
protected theorem precomp_uniformContinuous {𝔗 : Set (Set γ)} {f : γ → α} (hf : MapsTo (f '' ·) 𝔗 𝔖) :
UniformContinuous fun g : α →ᵤ[𝔖] β => ofFun 𝔗 (toFun 𝔖 g ∘ f) := by
-- This follows from the fact that `(· ∘ f) × (· ∘ f)` maps `gen (f '' t) V` to `gen t V`.
simp_rw [UniformContinuous, UniformOnFun.uniformity_eq, tendsto_iInf]
refine fun t ht V hV ↦ tendsto_iInf' (f '' t) <| tendsto_iInf' (hf ht) <| tendsto_iInf' V <| tendsto_iInf' hV ?_
simpa only [tendsto_principal_principal, UniformOnFun.gen] using fun _ ↦ forall_mem_image.1
