UniformEquiv.uniformContinuous
theorem UniformEquiv.uniformContinuous :
∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (h : α ≃ᵤ β),
UniformContinuous ⇑h
The theorem `UniformEquiv.uniformContinuous` asserts that for any two types `α` and `β`, both equipped with a uniform space structure, if there exists a uniform equivalence `h` between `α` and `β` (i.e., a bijection which is uniformly continuous in both directions), then the function `h` (casting from `α` to `β`) is uniformly continuous. That is, given any pair of points `x` and `y` close to each other in `α`, their images under `h` are close in `β` irrespective of the specific locations of `x` and `y` in `α`.
More concisely: If `h` is a uniform equivalence between uniform spaces `(α, δα)` and `(β, δβ)`, then `h` is a uniformly continuous function from `(α, δα)` to `(β, δβ)`.
|
UniformEquiv.uniformContinuous_toFun
theorem UniformEquiv.uniformContinuous_toFun :
∀ {α : Type u_4} {β : Type u_5} [inst : UniformSpace α] [inst_1 : UniformSpace β] (self : α ≃ᵤ β),
UniformContinuous self.toFun
This theorem states that for any two types `α` and `β` that are equipped with a uniform space structure, any uniformly equivalent function `self` from `α` to `β` is uniformly continuous. In other words, if a function `self` maps each point in `α` to a unique point in `β` and vice versa in a way that preserves the uniform structure, then this function `self` is uniformly continuous. This means that as points `x` and `y` in `α` get arbitrarily close to each other, their image points `self(x)` and `self(y)` in `β` also get arbitrarily close to each other, regardless of the actual positions of `x` and `y` in `α`.
More concisely: Given two uniform spaces `α` and `β` and a uniformly equivalent function `self` between them, `self` is a uniformly continuous function.
|
UniformEquiv.uniformContinuous_invFun
theorem UniformEquiv.uniformContinuous_invFun :
∀ {α : Type u_4} {β : Type u_5} [inst : UniformSpace α] [inst_1 : UniformSpace β] (self : α ≃ᵤ β),
UniformContinuous self.invFun
The theorem `UniformEquiv.uniformContinuous_invFun` states that for any two types `α` and `β`, each equipped with a UniformSpace structure, if there is a uniformly continuous bijection `self` from `α` to `β`, then the inverse function of `self` is also uniformly continuous. In other words, if a function is uniformly continuous when mapping from `α` to `β`, then it remains uniformly continuous when we reverse the direction of the mapping.
More concisely: If `f : α → β` is a uniformly continuous bijection between UniformSpaces `α` and `β`, then the inverse function `f⁻¹` is also uniformly continuous.
|