English
If u : α → γ is a uniform inducing map, then a family F is UniformEquicontinuous iff the composed family (u ∘ ·) ∘ F is UniformEquicontinuous.
Русский
Если u : α → γ — равномерно индуцирующая отображение, то семейство F равно равномерно экквинтино тогда и только тогда, когда композиция F с u остаётся равномерно экквинтиной.
LaTeX
$$$\\operatorname{UniformEquicontinuous} F \\iff \\operatorname{UniformEquicontinuous} ((u \\circ \\cdot) \\circ F).$$$
Lean4
theorem equicontinuousWithinAt_iff {κ₁ κ₂ : Type*} {p₁ : κ₁ → Prop} {s₁ : κ₁ → Set X} {p₂ : κ₂ → Prop}
{s₂ : κ₂ → Set (α × α)} {F : ι → X → α} {S : Set X} {x₀ : X} (hX : (𝓝[S] x₀).HasBasis p₁ s₁)
(hα : (𝓤 α).HasBasis p₂ s₂) :
EquicontinuousWithinAt F S x₀ ↔ ∀ k₂, p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ i, (F i x₀, F i x) ∈ s₂ k₂ :=
by
rw [equicontinuousWithinAt_iff_continuousWithinAt, ContinuousWithinAt,
hX.tendsto_iff (UniformFun.hasBasis_nhds_of_basis ι α _ hα)]
rfl
