English
If s is compact and f is continuous at every point of s, then f is uniformly continuous on s in a fiber-wise sense: for each q ∈ s and any entourage, there is a neighborhood of q in s such that nearby points p give uniform closeness of f(p, x) to f(q, x) for all x in the compact set k.
Русский
Если s компактно и f непрерывна в каждой точке s, то f равномерно непрерывна на s локально вдоль волокна: для каждого q ∈ s и каждого соседствия существует окрестность q в s, такая что для всех p в ней и всех x в компактном k выполняется близость f(p,x) к f(q,x).
LaTeX
$$$\\forall r \\in 𝓤\\beta\\; \\exists v \\in 𝓝[s]\,q, \\forall p \\in v, \\forall x \\in k, (f(p,x), f(q,x)) \\in r$$$
Lean4
/-- If `s` is compact and `f` is continuous at all points of `s`, then `f` is
"uniformly continuous at the set `s`", i.e. `f x` is close to `f y` whenever `x ∈ s` and `y` is
close to `x` (even if `y` is not itself in `s`, so this is a stronger assertion than
`UniformContinuousOn s`). -/
theorem uniformContinuousAt_of_continuousAt {r : Set (β × β)} {s : Set α} (hs : IsCompact s) (f : α → β)
(hf : ∀ a ∈ s, ContinuousAt f a) (hr : r ∈ 𝓤 β) : {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α :=
by
obtain ⟨t, ht, htsymm, htr⟩ := comp_symm_mem_uniformity_sets hr
choose U hU T hT hb using fun a ha =>
exists_mem_nhds_ball_subset_of_mem_nhds ((hf a ha).preimage_mem_nhds <| mem_nhds_left _ ht)
obtain ⟨fs, hsU⟩ := hs.elim_nhds_subcover' U hU
apply mem_of_superset ((biInter_finset_mem fs).2 fun a _ => hT a a.2)
rintro ⟨a₁, a₂⟩ h h₁
obtain ⟨a, ha, haU⟩ := Set.mem_iUnion₂.1 (hsU h₁)
apply htr
refine ⟨f a, htsymm.mk_mem_comm.1 (hb _ _ _ haU ?_), hb _ _ _ haU ?_⟩
exacts [mem_ball_self _ (hT a a.2), mem_iInter₂.1 h a ha]
