isUniformEmbedding — Mathlib

English

If a map is a uniform equivalence (uniformly bi-continuous and bijective with uniform inverse), then it is a uniform embedding.

Русский

Если отображение является равномерной эквивалентностью, то оно является равномерным вложением.

LaTeX

$$$\\displaystyle \\text{IsUniformEmbedding}(f)\\quad\\text{for } f:\\ α\\simeq β$$$

Lean4

theorem isUniformEmbedding {α β : Type*} [UniformSpace α] [UniformSpace β] (f : α ≃ β) (h₁ : UniformContinuous f)
    (h₂ : UniformContinuous f.symm) : IsUniformEmbedding f :=
  isUniformEmbedding_iff'.2 ⟨f.injective, h₁, by rwa [← Equiv.prodCongr_apply, ← map_equiv_symm]⟩

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