mapRingHom_coe — Mathlib

English

For a continuous ring hom f, and a ∈ α, the completion mapRingHom f hf applied to a (viewed inside the completion) equals f(a) mapped into the completion of β.

Русский

Для непрерывного кольцевого гомоморфизма f и элемента a ∈ α применение завершенного отображения mapRingHom f hf к a (в представлении внутри завершения) даёт значение f(a), приведённое в завершение β.

LaTeX

$$$$ (\mathrm{mapRingHom}\ f\ hf)(a) = (f(a)) \;\text{in} \;\widehat{\beta}, \quad a \in α $$$$

Lean4

theorem mapRingHom_coe (hf : UniformContinuous f) (a : α) : mapRingHom f hf.continuous a = f a := by
  rw [mapRingHom_apply, map_coe hf]

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