uniformContinuousOn_iff_restrict — Mathlib

English

For any f and s, UniformContinuousOn f s is equivalent to UniformContinuous (s.restrict f).

Русский

Для любых f и s UniformContinuousOn f s эквивалентно UniformContinuous (s.restrict f).

LaTeX

$$$$\\text{UniformContinuousOn } f\\; s \\;\\iff\\; \\text{UniformContinuous}(s.\\text{restrict } f).$$$$

Lean4

theorem uniformContinuousOn_iff_restrict [UniformSpace α] [UniformSpace β] {f : α → β} {s : Set α} :
    UniformContinuousOn f s ↔ UniformContinuous (s.restrict f) :=
  by
  delta UniformContinuousOn UniformContinuous
  rw [← map_uniformity_set_coe, tendsto_map'_iff]; rfl

Похожие утверждения