English
Construction of UniformFun.congrLeft includes that the left and right uniform continuity properties hold for precomposition with a bijection and its inverse, establishing a uniform equivalence.
Русский
Построение UniformFun.congrLeft обеспечивает равномерную непрерывность слева и справа для предсоставления через биекцию, образуя равномерное эквивалентное отображение.
LaTeX
$$$$ \text{Uniform equivalence via congrLeft: } (γ \cong α) \Rightarrow (UniformFun γ β) \simeq_{u} (UniformFun α β). $$$$
Lean4
/-- Turn a bijection `γ ≃ α` into a uniform isomorphism
`(γ →ᵤ β) ≃ᵤ (α →ᵤ β)` by pre-composing. -/
protected def congrLeft (e : γ ≃ α) : (γ →ᵤ β) ≃ᵤ (α →ᵤ β)
where
toEquiv := e.arrowCongr (.refl _)
uniformContinuous_toFun := UniformFun.precomp_uniformContinuous
uniformContinuous_invFun := UniformFun.precomp_uniformContinuous
