continuous_symm_iff — Mathlib

English

For an equivalence e, the symmetry map e.symm is continuous iff e is an open map.

Русский

Для эквивалентности e отображение-симметрическая часть e.symm непрерывна тогда и только тогда, когда e является открытым отображением.

LaTeX

$$$\mathrm{Continuous}(e^{-1}) \iff \mathrm{IsOpenMap}(e).$$$

Lean4

theorem continuous_symm_iff (e : X ≃ Y) : Continuous e.symm ↔ IsOpenMap e := by
  simp_rw [continuous_def, ← Set.image_equiv_eq_preimage_symm, IsOpenMap]

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