mem_range — Mathlib

English

Let f: M →ₗ⁅R,L⁆ N be a LieModuleHom and n ∈ N. Then n lies in the range of f if and only if there exists m ∈ M with f(m) = n.

Русский

Пусть f: M →ₗ⁅R,L⁆ N — гомоморфизм Ли-модуля и n ∈ N. Тогда n принадлежит образу f тогда и только тогда, когда ∃ m ∈ M such that f(m) = n.

LaTeX

$$$n \in f.range \iff \exists m, f(m) = n$$$

Lean4

@[simp]
theorem mem_range (n : N) : n ∈ f.range ↔ ∃ m, f m = n :=
  Iff.rfl

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