le_iff_uniformContinuous_id — Mathlib

English

An order relation u ≤ v between uniform spaces on α is equivalent to the identity map id: (α,u) → (α,v) being uniformly continuous.

Русский

Упорядочение u ≤ v для равномерных структур на α эквивалентно тому, что тождественное отображение id: (α,u) → (α,v) равномерно непрерывно.

LaTeX

$$u ≤ v ↔ UniformContinuous(id)$$

Lean4

theorem le_iff_uniformContinuous_id {u v : UniformSpace α} : u ≤ v ↔ @UniformContinuous _ _ u v id := by
  rw [uniformContinuous_iff, uniformSpace_comap_id, id]

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