continuousAt_extend_symm' — Mathlib

English

The extended inverse is continuous at the image of x for x in source.

Русский

Расширенная обратная карта непрерывна в образе x для x из источника.

LaTeX

$$$ {x \\in f.source} \\Rightarrow \\text{ContinuousAt}((f^{\\mathrm{extend}}_I)^{-1}, (f^{\\mathrm{extend}}_I)(x)). $$$

Lean4

theorem continuousAt_extend_symm' {x : E} (h : x ∈ (f.extend I).target) : ContinuousAt (f.extend I).symm x :=
  (f.continuousAt_symm h.2).comp I.continuous_symm.continuousAt

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