isOpenMap_val — Mathlib

English

The map val: Rˣ → R is an open map.

Русский

Отображение включения единиц в кольцо является открытым отображением.

LaTeX

$$$\\mathrm{IsOpenMap}(\\mathrm{val})$$$

Lean4

/-- In a normed ring with summable geometric series, the coercion from `Rˣ` (equipped with the
induced topology from the embedding in `R × R`) to `R` is an open map. -/
theorem isOpenMap_val : IsOpenMap (val : Rˣ → R) :=
  isOpenEmbedding_val.isOpenMap

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