isOpenMap_symm_iff

Mathlib.Topology.Continuous

URI: https://scilib.ai/kg/mathlib#Equiv.isOpenMap_symm_iff

English

For an equivalence e, IsOpenMap e.symm iff Continuous e.

Русский

Для эквивалентности e, IsOpenMap e.symm эквивалентно непрерывности e.

LaTeX

$$$\mathrm{IsOpenMap}(e.symm) \iff \mathrm{Continuous}(e).$$$

Lean4

theorem isOpenMap_symm_iff (e : X ≃ Y) : IsOpenMap e.symm ↔ Continuous e := by
  simp_rw [← Equiv.continuous_symm_iff, Equiv.symm_symm]

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

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

Разделы

Аффилиация

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