continuousOn_symm

Mathlib.Topology.OpenPartialHomeomorph

URI: https://scilib.ai/kg/mathlib#OpenPartialHomeomorph.continuousOn_symm

English

For an OpenPartialHomeomorph e, the inverse map e.symm is continuous on its target: ContinuousOn e.symm e.target.

Русский

Для открытого частичного гомеоморфа e обратная карта e.symm непрерывна на своей области: ContinuousOn e.symm e.target.

LaTeX

$$$\mathrm{ContinuousOn}(e.\mathrm{symm}, e.target).$$$

Lean4

theorem continuousOn_symm : ContinuousOn e.symm e.target :=
  e.continuousOn_invFun

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru