lift_of

Mathlib.RingTheory.AdicCompletion.Basic

URI: https://scilib.ai/kg/mathlib#Hausdorffification.lift_of

English

For any linear map f: M → N, evaluating lift I f on the image of x ∈ M via the canonical map of I M yields f x.

Русский

Для линейного отображения f: M → N функция lift I f на элементе of I M действует так, что lift I f (of I M x) = f x.

LaTeX

$$$\mathrm{lift}\ I\ f\ (\mathrm{of}\ I\ M\ x) = f\ x$$$

Lean4

theorem lift_of (f : M →ₗ[R] N) (x : M) : lift I f (of I M x) = f x :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru