uniformContinuous — Mathlib

English

On a space with the discrete uniformity, every function is uniformly continuous.

Русский

На пространстве с дискретной равномерностью любая функция является равномерно непрерывной.

LaTeX

$$$\forall Y,[UniformSpace Y],\ f:X\to Y: UniformContinuous f$$$

Lean4

/-- On a space with a discrete uniformity, any function is uniformly continuous. -/
theorem uniformContinuous {Y : Type*} [UniformSpace Y] (f : X → Y) : UniformContinuous f := by
  simp only [uniformContinuous_iff, DiscreteUniformity.eq_bot, bot_le]

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