toUniformEquivOfIsUniformInducing

English

A uniform inducing equivalence f: α ≃ β yields a uniform isomorphism α ≃ᵤ β.

Русский

Равномерный индуцирующий эквивалент f: α ≃ β даёт равномерный изоморфизм α ≃ᵤ β.

LaTeX

$$$\\text{toUniformEquivOfIsUniformInducing}(f) : α \\simeq_u β$$$

Lean4

/-- A uniform inducing equiv between uniform spaces is a uniform isomorphism. -/
def toUniformEquivOfIsUniformInducing [UniformSpace α] [UniformSpace β] (f : α ≃ β) (hf : IsUniformInducing f) :
    α ≃ᵤ β :=
  { f with
    uniformContinuous_toFun := hf.uniformContinuous
    uniformContinuous_invFun := hf.uniformContinuous_iff.2 <| by simpa using uniformContinuous_id }

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