English
If 𝔖 and 𝔗 are families of sets with a finite-union condition, the natural map (α →ᵤ[𝔗] β) → (α →ᵤ[𝔖] β) is uniformly continuous.
Русский
Если 𝔖 и 𝔗 удовлетворяют условию конечного объединения, естественный переходник между двумя пространствами является равномерно непрерывным.
LaTeX
$$$\text{UniformContinuous} (\mathrm{ofFun}\ 𝔗 \circ \mathrm{toFun}\ 𝔖)$ under the finite-union covering hypothesis.$$
Lean4
/-- If `𝔖` and `𝔗` are families of sets in `α`, then the identity map
`(α →ᵤ[𝔗] β) → (α →ᵤ[𝔖] β)` is uniformly continuous if every `s ∈ 𝔖` is contained in a finite
union of elements of `𝔗`.
With more API around `Order.Ideal`, this could be phrased in that language instead. -/
theorem uniformContinuous_ofFun_toFun (𝔗 : Set (Set α)) (h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T) :
UniformContinuous (ofFun 𝔗 ∘ toFun 𝔖 : (α →ᵤ[𝔗] β) → α →ᵤ[𝔖] β) :=
by
simp only [UniformContinuous, UniformOnFun.uniformity_eq, iInf₂_comm (ι₂ := Set (β × β))]
refine tendsto_iInf_iInf fun V ↦ tendsto_iInf_iInf fun hV ↦ ?_
simp only [tendsto_iInf, tendsto_principal, Filter.Eventually, mem_biInf_principal]
intro s hs
obtain ⟨T, hT𝔗, hT, hsT⟩ := h s hs
refine ⟨T, hT, hT𝔗, fun f hf ↦ ?_⟩
simp only [UniformOnFun.gen, Set.mem_iInter, Set.mem_setOf_eq, Function.comp_apply] at hf ⊢
intro x hx
obtain ⟨t, ht, hxt⟩ := Set.mem_sUnion.mp <| hsT hx
exact hf t ht x hxt
