mem_range — Mathlib

English

For a monoid hom f: G →* N and y ∈ N, y lies in the range of f if and only if there exists x ∈ G with f(x) = y.

Русский

Для гомоморфизма f: G →* N и элемента y ∈ N, y принадлежит образу f тогда и только тогда, когда существует x ∈ G такое, что f(x) = y.

LaTeX

$$$y \in \mathrm{Im}(f) \iff \exists x: G, f(x) = y$$$

Lean4

@[to_additive (attr := simp)]
theorem mem_range {f : G →* N} {y : N} : y ∈ f.range ↔ ∃ x, f x = y :=
  Iff.rfl

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