isOpenMap_toWeakSpace_symm — Mathlib

English

The inverse of the canonical weak-space embedding is an open map.

Русский

Обратное отображение канонического вложения в слабое пространство является открытым отображением.

LaTeX

$$$IsOpenMap\\ ((toWeakSpace 𝕜 E).symm)$$$

Lean4

/-- The canonical map from `WeakSpace 𝕜 E` to `E` is an open map. -/
theorem isOpenMap_toWeakSpace_symm : IsOpenMap (toWeakSpace 𝕜 E).symm :=
  IsOpenMap.of_inverse (toWeakSpaceCLM 𝕜 E).cont (toWeakSpace 𝕜 E).left_inv (toWeakSpace 𝕜 E).right_inv

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