English
Given a function f: α → β that is a uniform embedding, there exists a uniform equivalence between α and the range of f.
Русский
Для функции f: α → β, являющейся униформным вложением, существует униформное эквивалентство между α и множеством значений f.
LaTeX
$$$\\forall {\\alpha} {\\beta} [UniformSpace \\alpha] [UniformSpace \\beta] (f : \\alpha \\to \\beta) (hf : IsUniformEmbedding f),\\; \exists e: \\alpha \\simeq_u (Set.range f).Elem$$$
Lean4
/-- Uniform equiv given a uniform embedding. -/
noncomputable def ofIsUniformEmbedding (f : α → β) (hf : IsUniformEmbedding f) : α ≃ᵤ Set.range f
where
uniformContinuous_toFun := hf.isUniformInducing.uniformContinuous.subtype_mk _
uniformContinuous_invFun :=
by
rw [hf.isUniformInducing.uniformContinuous_iff, Equiv.invFun_as_coe, Equiv.self_comp_ofInjective_symm]
exact uniformContinuous_subtype_val
toEquiv := Equiv.ofInjective f hf.injective
