mapRingHom_apply — Mathlib

English

For every x in the completion of α, the extension mapRingHom f hf evaluated at x coincides with the natural extension of f to the completion of β.

Русский

Для любого элемента x в завершении α значение розширенного отображения mapRingHom f hf в x совпадает с естественным продолжением f к завершению β.

LaTeX

$$$$ (\mathrm{mapRingHom}\ f\ hf)\,x = \mathrm{map} f\,x, \quad x \in \widehat{\alpha} $$$$

Lean4

theorem mapRingHom_apply {x : UniformSpace.Completion α} :
    UniformSpace.Completion.mapRingHom f hf x = UniformSpace.Completion.map f x :=
  rfl

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