uniformContinuousOn_univ — Mathlib

English

Uniform continuity on the entire domain and uniform continuity on the whole space coincide: UniformContinuousOn f univ ↔ UniformContinuous f.

Русский

Униформная непрерывность на множестве равна униформной непрерывности на всём пространстве: UniformContinuousOn f univ ⇔ UniformContinuous f.

LaTeX

$$$ UniformContinuousOn(f,\mathsf{univ}) \;\iff\; UniformContinuous f. $$$

Lean4

theorem uniformContinuousOn_univ [UniformSpace β] {f : α → β} : UniformContinuousOn f univ ↔ UniformContinuous f := by
  rw [UniformContinuousOn, UniformContinuous, univ_prod_univ, principal_univ, inf_top_eq]

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