congrRight — Mathlib

English

Post-composing by a uniform isomorphism yields a uniform isomorphism between the corresponding 𝔖-convergence spaces.

Русский

Пост-композиция по равномерной изоморфизму задаёт равномерную изоморфность между пространствами 𝔖-конвергенций.

LaTeX

$$UniformOnFun.congrRight {f : γ ≃ᵤ β} : (α →ᵤ[𝔖] γ) ≃ᵤ (α →ᵤ[𝔖] β).$$

Lean4

/-- Turn a uniform isomorphism `γ ≃ᵤ β` into a uniform isomorphism `(α →ᵤ[𝔖] γ) ≃ᵤ (α →ᵤ[𝔖] β)`
by post-composing. -/
protected def congrRight [UniformSpace γ] (e : γ ≃ᵤ β) : (α →ᵤ[𝔖] γ) ≃ᵤ (α →ᵤ[𝔖] β) :=
  {
    Equiv.piCongrRight fun _a =>
      e.toEquiv with
    uniformContinuous_toFun := UniformOnFun.postcomp_uniformContinuous e.uniformContinuous
    uniformContinuous_invFun := UniformOnFun.postcomp_uniformContinuous e.symm.uniformContinuous }

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