English
Uniform isomorphism between α^2 and α × α, built via a fixed equivalence finTwoArrowEquiv.
Русский
Равномерный изоморфизм между α^2 и α × α конструируется через фиксированное эквивалентное отображение finTwoArrowEquiv.
LaTeX
$$$(\\text{Fin } 2 \\to α) \\cong_{u} α × α$$$
Lean4
/-- A subset of a uniform space is uniformly isomorphic to its image under a uniform isomorphism.
-/
def image (e : α ≃ᵤ β) (s : Set α) : s ≃ᵤ e '' s
where
uniformContinuous_toFun := (e.uniformContinuous.comp uniformContinuous_subtype_val).subtype_mk _
uniformContinuous_invFun := (e.symm.uniformContinuous.comp uniformContinuous_subtype_val).subtype_mk _
toEquiv := e.toEquiv.image s
