isOpenEmbedding_val — Mathlib

English

In a normed ring with summable geometric series, the inclusion map val: Rˣ → R is an open embedding.

Русский

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

LaTeX

$$$\\mathrm{IsOpenEmbedding}(\\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 embedding. -/
theorem isOpenEmbedding_val : IsOpenEmbedding (val : Rˣ → R)
    where
  toIsEmbedding :=
    isEmbedding_val_mk' (fun _ ⟨u, hu⟩ ↦ hu ▸ (inverse_continuousAt u).continuousWithinAt) Ring.inverse_unit
  isOpen_range := Units.isOpen

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