comap_comap

Mathlib.Topology.Algebra.Module.ClosedSubmodule

URI: https://scilib.ai/kg/mathlib#ClosedSubmodule.comap_comap

English

Repeated: the identity preimage does not change a closed submodule.

Русский

Повтор: предобраз тождественного отображения не меняет замкнутый подпмодуль.

LaTeX

$$$s.comap (\mathrm{id}_{R}) = s$$$

Lean4

theorem comap_comap (g : N →L[R] O) (f : M →L[R] N) (s : ClosedSubmodule R O) :
    (s.comap g).comap f = s.comap (g.comp f) :=
  rfl

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

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

Разделы

Аффилиация

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