continuous_symm — Mathlib

English

Let α and β be uniform spaces and h: α ≃ᵤ β a uniform equivalence. Then the inverse map h^{-1}: β → α is continuous.

Русский

Пусть α и β — равномерные пространства, и h: α ≃ᵤ β — равномерное эквивалентство. Тогда обратная карта h^{-1}: β → α непрерывна.

LaTeX

$$$\\forall \\alpha \\beta [UniformSpace \\alpha] [UniformSpace \\beta] (h : \\alpha \\simeq_u \\beta),\\; Continuous(h^{-1})$$$

Lean4

@[continuity]
protected theorem continuous_symm (h : α ≃ᵤ β) : Continuous h.symm :=
  h.uniformContinuous_symm.continuous

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