uniformContinuous_completionSeparationQuotientEquiv_symm

English

The inverse of the completionSeparationQuotientEquiv is uniformly continuous.

Русский

Обратное эквив между завершениями имеет свойство равномерной непрерывности.

LaTeX

$$$\\mathrm{UniformContinuous}\left( \\left( \\mathrm{completionSeparationQuotientEquiv}(\\alpha) \\right)^{-1} \\right)$$$

Lean4

theorem uniformContinuous_completionSeparationQuotientEquiv_symm :
    UniformContinuous (completionSeparationQuotientEquiv α).symm :=
  uniformContinuous_map

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