map_bracket_eq — Mathlib

English

For a LieModule M, map f of bracket [I,N] equals bracket I of map f N: map f [I,N] = [I, map f N].

Русский

Для Ли-модуля M отображение f скобки [I,N] равно скобке [I, map f N].

LaTeX

$$$$ \operatorname{map} f \big( [I,N] \big) = [I, \operatorname{map} f N]. $$$$

Lean4

theorem map_bracket_eq [LieModule R L M] : map f ⁅I, N⁆ = ⁅I, map f N⁆ :=
  by
  rw [← toSubmodule_inj, toSubmodule_map, lieIdeal_oper_eq_linear_span, lieIdeal_oper_eq_linear_span,
    Submodule.map_span]
  congr
  ext m
  simp

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