English
Let ha be HasBasis for 𝓤 α and hb HasBasis for 𝓤 β. Then UniformContinuousOn f S is equivalent to a pointwise basis condition with S included: ∀ i, q i → ∃ j, p j ∧ ∀ x ∈ S, ∀ y ∈ S, (x,y) ∈ s j → (f x, f y) ∈ t i.
Русский
Пусть ha и hb — базы 𝓤 α и 𝓤 β. Тогда UniformContinuousOn f S эквивалентно условию на пары элементов S.
LaTeX
$$$\text{UniformContinuousOn } f S \;\iff\; \forall i, q i \to \exists j, p j \land \forall x \in S, \forall y \in S, (x,y) \in s j \to (f x, f y) \in t i.$$$
Lean4
theorem uniformContinuousOn_iff {ι'} [UniformSpace β] {p : ι → Prop} {s : ι → Set (α × α)} (ha : (𝓤 α).HasBasis p s)
{q : ι' → Prop} {t : ι' → Set (β × β)} (hb : (𝓤 β).HasBasis q t) {f : α → β} {S : Set α} :
UniformContinuousOn f S ↔ ∀ i, q i → ∃ j, p j ∧ ∀ x, x ∈ S → ∀ y, y ∈ S → (x, y) ∈ s j → (f x, f y) ∈ t i :=
((ha.inf_principal (S ×ˢ S)).tendsto_iff hb).trans <| by
simp_rw [Prod.forall, Set.inter_comm (s _), forall_mem_comm, mem_inter_iff, mem_prod, and_imp]
