coe_map_toEnd_le — Mathlib

English

The image of a LieSubmodule under the map to End R L M lies below the ambient submodule, i.e., the map preserves the submodule inclusion order.

Русский

Образ подмодуля Ли через отображение к End сохраняет порядок включения: изображение подмодуля находится внутри общего подмодуля.

LaTeX

$$$(N :\!\ Submodule\ R M).map (\mathrm{toEnd}_{R,L,M} x) \le N$$$

Lean4

theorem coe_map_toEnd_le : (N : Submodule R M).map (LieModule.toEnd R L M x) ≤ N :=
  by
  rintro n ⟨m, hm, rfl⟩
  exact N.lie_mem hm

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