continuous_diracProbaEquivSymm — Mathlib

English

The inverse of the forward continuous equivalence is continuous.

Русский

Обратное отображение непрерывной эквив направлено непрерывно.

LaTeX

$$$\\text{Continuous}(\\mathrm{diracProbaEquiv}^{-1})$$$

Lean4

/-- In a completely regular T0 topological space, the inverse of `diracProbaEquiv` is continuous. -/
theorem continuous_diracProbaEquivSymm [T0Space X] [CompletelyRegularSpace X] :
    Continuous (diracProbaEquiv (X := X)).symm :=
  by
  apply continuous_iff_continuousAt.mpr
  intro μ
  apply continuousAt_of_tendsto_nhds (y := diracProbaInverse μ)
  exact (tendsto_diracProbaEquivSymm_iff_tendsto _).mpr fun _ mem_nhds ↦ mem_nhds

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