English
The uniform equivalence between C(X, R)₀ and C(Y, R)₀ is induced by a homeomorphism f: X ≃ₜ Y sending 0 to 0, with explicit uniform-continuous structure for both directions.
Русский
Унитарное равномерное соответствие между C(X, R)₀ и C(Y, R)₀ задаётся левой стрелкой через гомоморфизм f: X ≃ₜ Y с f(0)=0, с явной равномерной непрерывностью в обе стороны.
LaTeX
$$$\text{UniformEquiv.arrowCongrLeft₀} (f) : C(X,R)₀ \simeqᵤ C(Y,R)₀$$$
Lean4
/-- The uniform equivalence `C(X, R)₀ ≃ᵤ C(Y, R)₀` induced by a homeomorphism of the domains
sending `0 : X` to `0 : Y`. -/
def _root_.UniformEquiv.arrowCongrLeft₀ {Y : Type*} [TopologicalSpace Y] [Zero Y] (f : X ≃ₜ Y) (hf : f 0 = 0) :
C(X, R)₀ ≃ᵤ C(Y, R)₀
where
toFun g := g.comp ⟨f.symm, (f.toEquiv.apply_eq_iff_eq_symm_apply.eq ▸ hf).symm⟩
invFun g := g.comp ⟨f, hf⟩
left_inv g := ext fun _ ↦ congrArg g <| f.left_inv _
right_inv g := ext fun _ ↦ congrArg g <| f.right_inv _
uniformContinuous_toFun :=
isUniformEmbedding_toContinuousMap.uniformContinuous_iff.mpr <|
ContinuousMap.uniformContinuous_comp_left (f.symm : C(Y, X)) |>.comp
isUniformEmbedding_toContinuousMap.uniformContinuous
uniformContinuous_invFun :=
isUniformEmbedding_toContinuousMap.uniformContinuous_iff.mpr <|
ContinuousMap.uniformContinuous_comp_left (f : C(X, Y)) |>.comp
isUniformEmbedding_toContinuousMap.uniformContinuous
