map_incl_top

Mathlib.Algebra.Lie.Submodule

URI: https://scilib.ai/kg/mathlib#LieSubmodule.map_incl_top

English

Mapping the top submodule along the inclusion map yields the original submodule.

Русский

Отображение вершины подмодуля по включению даёт исходный подмодуль.

LaTeX

$$$\left(\top : \mathrm{LieSubmodule}\, R\, L\, N\right).map N.incl = N$$$

Lean4

theorem map_incl_top : (⊤ : LieSubmodule R L N).map N.incl = N := by simp

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

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

Разделы

Аффилиация

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