continuousOn_extend_symm — Mathlib

English

The preimage under the extended chart of an open set is open in the extended source.

Русский

Обратное изображение открытого множества под расширенным чартом открыто в расширенном источнике.

LaTeX

$$$ (f^{\\mathrm{extend}}_I)^{-1}[s] \\cap (f^{\\mathrm{extend}}_I).\\mathrm{source} \\text{ is open for } s \\text{ open.}$$$

Lean4

theorem continuousOn_extend_symm : ContinuousOn (f.extend I).symm (f.extend I).target := fun _ h =>
  (continuousAt_extend_symm' _ h).continuousWithinAt

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