English
Let ha and hb be HasBasis representations of 𝓤 α and 𝓤 β. Then f is UniformContinuous iff for every i with q i there exists j with p j such that ∀ x,y in α, (x,y) ∈ s j implies (f x, f y) ∈ t i.
Русский
Пусть ha, hb задают базы базовых окружностей 𝓤 α и 𝓤 β. Тогда f равномерно непрерывна ⟺ ∀ i с q i ∃ j с p j: ∀ x,y ∈ α, если (x,y) ∈ s j, то (f x, f y) ∈ t i.
LaTeX
$$$\text{UniformContinuous } f \iff \forall i, q i \to \exists j, p j \land \forall x,y, (x,y)\in s j \to (f x,f y)\in t i.$$$
Lean4
theorem uniformContinuous_iff {ι'} [UniformSpace β] {p : ι → Prop} {s : ι → Set (α × α)} (ha : (𝓤 α).HasBasis p s)
{q : ι' → Prop} {t : ι' → Set (β × β)} (hb : (𝓤 β).HasBasis q t) {f : α → β} :
UniformContinuous f ↔ ∀ i, q i → ∃ j, p j ∧ ∀ x y, (x, y) ∈ s j → (f x, f y) ∈ t i :=
(ha.tendsto_iff hb).trans <| by simp only [Prod.forall]
