mapIncl_def — Mathlib

English

The mapIncl for submodules equals the map built from the respective inclusions: mapIncl(M',N') = map(M'.incl, N'.incl).

Русский

Отображение включения подмодулей равно отображению, построенному из соответствующих включений: mapIncl(M',N') = map(M'.incl, N'.incl).

LaTeX

$$$\mathrm{mapIncl}\,M'\,N' = \mathrm{map}\,\big(M'.\mathrm{incl},\; N'.\mathrm{incl}\big).$$$

Lean4

@[simp]
theorem mapIncl_def (M' : LieSubmodule R L M) (N' : LieSubmodule R L N) : mapIncl M' N' = map M'.incl N'.incl :=
  rfl

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