coe_range — Mathlib

English

Let f be a Lie module homomorphism f: M →ₗ⁅R,L⁆ N. Then the range of f, viewed as a Lie submodule of N, coincides with the set of all values f(m) as m runs through M; equivalently, the underlying set of f.range is exactly Set.range f.

Русский

Пусть f: M →ₗ⁅R,L⁆ N — гомоморфизм Ли-модулей. Тогда образ f, рассматриваемый как подмодуль N, совпадает с множеством всех значений f(m), где m пробегает по M; эквивалентно, множество значений f.range совпадает с Set.range f.

LaTeX

$$$f.range = \{ f(m) \mid m \in M \} = \mathrm{Im}(f)$$$

Lean4

@[simp]
theorem coe_range : f.range = Set.range f :=
  rfl

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