Pointwise convergence and total boundedness for equicontinuous families

Mathlib's EquicontinuousOn.tendsto_uniformOnFun_iff_pi' identifies, for families equicontinuous on compact sets, uniform convergence on those sets with pointwise convergence on their union. EquicontinuousOn.tendstoUniformlyOn_of_tendsto states the direction used in practice for a single compact set, in terms of TendstoUniformlyOn. Combined with LipschitzWith.uniformEquicontinuous, it shows that equi-Lipschitz functions converging pointwise converge uniformly on compact sets.

EquicontinuousWithinAt.totallyBounded_range_eval spreads total boundedness of the values of a family from a set of points D to any point of the closure of D at which the family is equicontinuous within D. It is the pointwise step of the Arzelà–Ascoli theorem with a dense set of points.

theorem EquicontinuousOn.tendstoUniformlyOn_of_tendsto {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} {K : Set X} (hF : EquicontinuousOn F K) (hK : IsCompact K) {L : Filter ι} {f : X → α} (hFf : ∀ x ∈ K, Filter.Tendsto (fun (i : ι) => F i x) L (nhds (f x))) : TendstoUniformlyOn F f L K

A family equicontinuous on a compact set K and converging pointwise on K converges uniformly on K.

theorem EquicontinuousWithinAt.totallyBounded_range_eval {ι : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [UniformSpace Y] {F : ι → X → Y} {D : Set X} {x : X} (hF : EquicontinuousWithinAt F D x) (hx : x ∈ closure D) (hFD : ∀ x ∈ D, TotallyBounded (Set.range fun (i : ι) => F i x)) : TotallyBounded (Set.range fun (i : ι) => F i x)

Equicontinuity within D at a point x of the closure of D spreads total boundedness of the values from the points of D to x.