tendsto_symm — Mathlib

English

As x varies in the source, the inverse map e.symm tends neighborhoods of e(x) to neighborhoods of x.

Русский

При изменении x в источнике, обратное отображение e.symm стягивает окрестности e(x) в окрестности x.

LaTeX

$$$\\forall x: \\mathrm{Tendsto}(e^{-1}, \\mathcal{N}(e(x)), \\mathcal{N}(x))$$$

Lean4

theorem tendsto_symm {x} (hx : x ∈ e.source) : Tendsto e.symm (𝓝 (e x)) (𝓝 x) := by
  simpa only [ContinuousAt, e.left_inv hx] using e.continuousAt_symm (e.map_source hx)

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