English
The continuities of functions are equivalent to pointwise continuities of coordinate maps; there are several equivalent reformulations using tendsto/uniform tendsto.
Русский
Существуют эквивалентности между непрерывностью функций и по координатам непрерывностью; эквивалентности формулируются через пределы и равномерности.
LaTeX
$$UniformOnFun.continuous_rng_iff {X} {Y} ...$$
Lean4
protected theorem continuous_rng_iff {X : Type*} [TopologicalSpace X] {f : X → (α →ᵤ[𝔖] β)} :
Continuous f ↔ ∀ s ∈ 𝔖, Continuous (UniformFun.ofFun ∘ s.restrict ∘ UniformOnFun.toFun 𝔖 ∘ f) := by
simp only [continuous_iff_continuousAt, ContinuousAt, UniformOnFun.tendsto_iff_tendstoUniformlyOn,
UniformFun.tendsto_iff_tendstoUniformly, tendstoUniformlyOn_iff_tendstoUniformly_comp_coe, @forall_swap X,
Function.comp_def, restrict_eq, UniformFun.toFun_ofFun]
