toContinuousMap_X_eq_id — Mathlib

English

Let R be a topological semiring. The indeterminate X, viewed as a polynomial in R[X], yields the identity map on R as a continuous map: X.toContinuousMap = id_R.

Русский

Пусть R — топологическое полускольцо. Индетерминанта X, рассмотренная как полином R[X], задаёт тождественное непрерывное отображение R → R: X.toContinuousMap = id_R.

LaTeX

$$$ X.toContinuousMap = \\mathrm{id}\\,R $$$

Lean4

theorem toContinuousMap_X_eq_id : X.toContinuousMap = .id R := by ext; simp

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