continuousAt_symm — Mathlib

English

The inverse map e.symm is continuous at every point of its target.

Русский

Обратная карта e.symm непрерывна во всех точках своей области значений.

LaTeX

$$$\\forall x \\in \\mathrm{target}(e): \\mathrm{ContinuousAt}(e, x)^{\\mathrm{symm}}$$$

Lean4

/-- An open partial homeomorphism inverse is continuous at any point of its target -/
theorem continuousAt_symm {x : Y} (h : x ∈ e.target) : ContinuousAt e.symm x :=
  e.symm.continuousAt h

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